Article

VeriFast: a powerful, sound, predictable, fast verifier for C and java

Authors:

Frank PiessensAuthors Info & Claims

NFM'11: Proceedings of the Third international conference on NASA Formal methods

Pages 41 - 55

Published: 18 April 2011 Publication History

Publisher Site

Abstract

VeriFast is a prototype verification tool for single-threaded and multithreaded C and Java programs. In this paper, we first describe the basic symbolic execution approach in some formal detail. Then we zoom in on two technical aspects: the approach to permission accounting, including fractional permissions, precise predicates, and counting permissions; and the approach to lemma function termination in the presence of dynamically-bound lemma function calls. Finally, we describe three ongoing efforts: application to JavaCard programs, integration of shape analysis, and application to Linux device drivers.

References

[1]

Jacobs, B., Smans, J., Piessens, F.: A quick tour of the veriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304-311. Springer, Heidelberg (2010).

Digital Library

Google Scholar

[2]

Jacobs, B., Smans, J., Piessens, F.: The VeriFast program verifier: A tutorial (2010), http://www.cs.kuleuven.be/~bartj/verifast/

Google Scholar

[3]

Bornat, R., Calcagno, C., O'Hearn, P., Parkinson, M.: Permission accounting in separation logic. In: POPL (2005).

Digital Library

Google Scholar

[4]

Jacobs, B., Piessens, F.: Expressive modular fine-grained concurrency specification. In: POPL (2011).

Digital Library

Google Scholar

[5]

Distefano, D., O'Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 287-302. Springer, Heidelberg (2006).

Digital Library

Google Scholar

[6]

Calcagno, C., Distefano, D., O'Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: POPL (2009).

Digital Library

Google Scholar

Cited By

View all

Pirelli SZaostrovnykh ACandea G(2019)A formally verified NAT stackACM SIGCOMM Computer Communication Review10.1145/3310165.331017648:5(77-83)Online publication date: 28-Jan-2019
https://dl.acm.org/doi/10.1145/3310165.3310176
Blanchard AKosmatov NLoulergue FHung CPapadopoulos G(2019)Logic against ghostsProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297495(2186-2195)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297495
Polikarpova NSergey I(2019)Structuring the synthesis of heap-manipulating programsProceedings of the ACM on Programming Languages10.1145/32903853:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290385
Show More Cited By

Recommendations

Software verification with VeriFast: Industrial case studies

In this article, we present a series of four industrial case studies in software verification. We applied VeriFast, a sound and modular software verifier based on separation logic, to two Java Card smart card applets, a Linux device driver, and an ...
Solving the VerifyThis 2012 challenges with VeriFast

We describe our experience solving the VerifyThis 2012 challenges with our program verification tool VeriFast, including detailed explanations of our solutions. We also describe some alternative solutions that we developed after the competition. ...
A quick tour of the VeriFast program verifier
APLAS'10: Proceedings of the 8th Asian conference on Programming languages and systems

This paper describes the main features of VeriFast, a sound and modular program verifier for C and Java. VeriFast takes as input a number of source files annotated with method contracts written in separation logic, inductive data type and fixpoint ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

NFM'11: Proceedings of the Third international conference on NASA Formal methods

April 2011

531 pages

ISBN:9783642203978

Editors:
Mihaela Bobaru
NASA Jet Propulsion Laboratory, Pasadena, CA
,
Klaus Havelund
NASA Jet Propulsion Laboratory, Pasadena, CA
,
Gerard J. Holzmann
NASA Jet Propulsion Laboratory, Pasadena, CA
,
Rajeev Joshi
NASA Jet Propulsion Laboratory, Pasadena, CA

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 18 April 2011

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

68
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Pirelli SZaostrovnykh ACandea G(2019)A formally verified NAT stackACM SIGCOMM Computer Communication Review10.1145/3310165.331017648:5(77-83)Online publication date: 28-Jan-2019
https://dl.acm.org/doi/10.1145/3310165.3310176
Blanchard AKosmatov NLoulergue FHung CPapadopoulos G(2019)Logic against ghostsProceedings of the 34th ACM/SIGAPP Symposium on Applied Computing10.1145/3297280.3297495(2186-2195)Online publication date: 8-Apr-2019
https://dl.acm.org/doi/10.1145/3297280.3297495
Polikarpova NSergey I(2019)Structuring the synthesis of heap-manipulating programsProceedings of the ACM on Programming Languages10.1145/32903853:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290385
Fragoso Santos JMaksimović PSampaio GGardner P(2019)JaVerT 2.0: compositional symbolic execution for JavaScriptProceedings of the ACM on Programming Languages10.1145/32903793:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290379
Peterson CLaBorde PDechev DGuéhéneuc YKhomh FSarro F(2019)CCSpecProceedings of the 27th International Conference on Program Comprehension10.1109/ICPC.2019.00041(220-230)Online publication date: 25-May-2019
https://dl.acm.org/doi/10.1109/ICPC.2019.00041
Pauget BPearce DPotanin AKell SMarr S(2018)Towards compilation of an imperative language for FPGAsProceedings of the 10th ACM SIGPLAN International Workshop on Virtual Machines and Intermediate Languages10.1145/3281287.3281291(47-56)Online publication date: 4-Nov-2018
https://dl.acm.org/doi/10.1145/3281287.3281291
Blackshear SGorogiannis NO'Hearn PSergey I(2018)RacerD: compositional static race detectionProceedings of the ACM on Programming Languages10.1145/32765142:OOPSLA(1-28)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276514
Besson FDang AJensen TAlvim MDelaune S(2018)Securing Compilation Against Memory ProbingProceedings of the 13th Workshop on Programming Languages and Analysis for Security10.1145/3264820.3264822(29-40)Online publication date: 15-Oct-2018
https://dl.acm.org/doi/10.1145/3264820.3264822
Santos JMaksimović PGrohens TDolby JGardner PSabel DThiemann P(2018)Symbolic Execution for JavaScriptProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236956(1-14)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236956
Joosten SOortwijn WSafari MHuisman MDolby JHalfond WMishra A(2018)An exercise in verifying sequential programs with VerCorsCompanion Proceedings for the ISSTA/ECOOP 2018 Workshops10.1145/3236454.3236479(40-45)Online publication date: 16-Jul-2018
https://dl.acm.org/doi/10.1145/3236454.3236479
Show More Cited By

Abstract

References

Cited By

Recommendations

Software verification with VeriFast: Industrial case studies

Solving the VerifyThis 2012 challenges with VeriFast

A quick tour of the VeriFast program verifier

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations