KIV: overview and VerifyThis competition
Members of our research group participated in the VerifyThis competition at FM 2012 in
Paris using the interactive specification and verification system KIV. In this article we …
Paris using the interactive specification and verification system KIV. In this article we …
TOOLympics 2019: An overview of competitions in formal methods
Abstract Evaluation of scientific contributions can be done in many different ways. For the
various research communities working on the verification of systems (software, hardware, or …
various research communities working on the verification of systems (software, hardware, or …
Autoproof: Auto-active functional verification of object-oriented programs
Auto-active verifiers provide a level of automation intermediate between fully automatic and
interactive: users supply code with annotations as input while benefiting from a high level of …
interactive: users supply code with annotations as input while benefiting from a high level of …
Lessons learned from microkernel verification--specification is the new bottleneck
Software verification tools have become a lot more powerful in recent years. Even
verification of large, complex systems is feasible, as demonstrated in the L4. verified and …
verification of large, complex systems is feasible, as demonstrated in the L4. verified and …
VerifyThis 2012: A program verification competition
VerifyThis 2012 was a 2-day verification competition that took place as part of the
International Symposium on Formal Methods (FM 2012) on August 30–31, 2012, in Paris …
International Symposium on Formal Methods (FM 2012) on August 30–31, 2012, in Paris …
A complete approach to loop verification with invariants and summaries
G Ernst - arXiv preprint arXiv:2010.05812, 2020 - arxiv.org
Invariants are the predominant approach to verify the correctness of loops. As an alternative,
loop contracts, which make explicit the premise and conclusion of the underlying induction …
loop contracts, which make explicit the premise and conclusion of the underlying induction …
[HTML][HTML] Designing a verifying compiler: Lessons learned from developing whiley
DJ Pearce, L Groves - Science of Computer Programming, 2015 - Elsevier
An ongoing challenge for computer science is the development of a tool which automatically
verifies programs meet their specifications, and are free from runtime errors such as divide …
verifies programs meet their specifications, and are free from runtime errors such as divide …
VerifyThis–verification competition with a human factor
VerifyThis is a series of competitions that aims to evaluate the current state of deductive tools
to prove functional correctness of programs. Such proofs typically require human creativity …
to prove functional correctness of programs. Such proofs typically require human creativity …
Loop verification with invariants and contracts
G Ernst - … Conference on Verification, Model Checking, and …, 2022 - Springer
Invariants are the predominant approach to verify the correctness of loops. As an alternative,
loop contracts, which make explicit the premise and conclusion of the underlying induction …
loop contracts, which make explicit the premise and conclusion of the underlying induction …
Integrated environment for diagnosing verification errors
M Christakis, KRM Leino, P Müller… - … 2016, Held as Part of the …, 2016 - Springer
A failed attempt to verify a program's correctness can result in reports of genuine errors,
spurious warnings, and timeouts. The main challenge in debugging a verification failure is to …
spurious warnings, and timeouts. The main challenge in debugging a verification failure is to …