uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
JayHorn: A framework for verifying Java programs
Nasa Ames CMU, Moffett Field, CA USA.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems. (Embedded Systems)ORCID iD: 0000-0002-2733-7098
SRI Int, 333 Ravenswood Ave, Menlo Pk, CA 94025 USA.
SRI Int, 333 Ravenswood Ave, Menlo Pk, CA 94025 USA.
2016 (English)In: Computer Aided Verification: Part I, Springer, 2016, p. 352-358Conference paper, Published paper (Refereed)
Abstract [en]

Building a competitive program verifiers is becoming cheaper. On the front-end side, openly available compiler infrastructure and optimization frameworks take care of hairy problems such as alias analysis, and break down the subtleties of modern languages into a handful of simple instructions that need to be handled. On the back-end side, theorem provers start providing full-fledged model checking algorithms, such as PDR, that take care looping control-flow. In this spirit, we developed JayHorn, a verification framework for Java with the goal of having as few moving parts as possible. Most steps of the translation from Java into logic are implemented as bytecode transformations, with the implication that their soundness can be tested easily. From the transformed bytecode, we generate a set of constrained Horn clauses that are verified using state-of-the-art Horn solvers. We report on our implementation experience and evaluate JayHorn on benchmarks.

Place, publisher, year, edition, pages
Springer, 2016. p. 352-358
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9779
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-309991DOI: 10.1007/978-3-319-41528-4_19ISI: 000387731200019ISBN: 9783319415277 (print)OAI: oai:DiVA.org:uu-309991DiVA, id: diva2:1054694
Conference
CAV 2016, July 17–23, Toronto, Canada
Funder
Swedish Research Council, 2014-5484Available from: 2016-07-13 Created: 2016-12-08 Last updated: 2018-01-13Bibliographically approved

Open Access in DiVA

fulltext(701 kB)162 downloads
File information
File name FULLTEXT01.pdfFile size 701 kBChecksum SHA-512
2d3990d8db73e9d8614bbafde9b1e7661c0381c86cbd775375b1c58d8200803749d7703e919be0628f3d0cf84c4f369e9d37d0fda27a6d7964f1540005301715
Type fulltextMimetype application/pdf

Other links

Publisher's full text

Authority records BETA

Rümmer, Philipp

Search in DiVA

By author/editor
Rümmer, Philipp
By organisation
Computer Systems
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 162 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 474 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf