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 Java Model Checker
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computer Systems.ORCID iD: 0000-0002-2733-7098
2019 (English)In: PROCEEDINGS OF THE 21ST WORKSHOP ON FORMAL TECHNIQUES FOR JAVA-LIKE PROGRAMS (FTFJP 2019), ASSOC COMPUTING MACHINERY , 2019, article id 1Conference paper, Oral presentation with published abstract (Refereed)
Abstract [en]

This talk will give an overview of the JayHorn verification tool, a model checker for sequential Java programs annotated with assertions expressing safety conditions. JayHorn is fully automatic and based to a large degree on standard infrastructure for compilation and verification: it uses the Soot library as front-end to read Java bytecode and translate it to the Jimple three-address format, and the state-of-the-art Horn solvers SPACER and Eldarica as back-ends that infer loop invariants, object and class invariants, and method contracts. Since JayHorn uses an invariant-based representation of heap data-structures, it is particularly useful for analysing programs with unbounded data-structures and unbounded run-time, while at the same time avoiding the use of logical theories, like the theory of arrays, often considered hard for Horn solvers. The development of JayHorn is ongoing, and the talk will also cover some of the future features of JayHorn, in particular the handling of strings.

Place, publisher, year, edition, pages
ASSOC COMPUTING MACHINERY , 2019. article id 1
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-403022DOI: 10.1145/3340672.3341113ISI: 000505151200001ISBN: 978-1-4503-6864-3 (print)OAI: oai:DiVA.org:uu-403022DiVA, id: diva2:1388459
Conference
21st Workshop on Formal Techniques for Java-Like Programs (FTfJP), JUL 15, 2019, London, ENGLAND
Funder
Swedish Research Council, 2014-5484Swedish Research Council, 20184727Swedish Foundation for Strategic Research , RIT17-0011Available from: 2020-01-24 Created: 2020-01-24 Last updated: 2020-01-24Bibliographically approved

Open Access in DiVA

No full text in DiVA

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

doi
isbn
urn-nbn

Altmetric score

doi
isbn
urn-nbn
Total: 7 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