LCTD: test-guided proofs for C programs on LLVM

DOI10.1016/J.JLAMP.2015.10.010zbMATHOpenAlexWikidataMaRDI QIDQ338629FDO

Authors Olli Saarikivi, Keijo Heljanko

Publication date 7 November 2016

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2015.10.010

zbMATH Keywords

verificationabstraction refinementautomated testingdynamic symbolic executionpredicate abstractionweakest precondition

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 1982210
• Dafny: an automatic program verifier for functional correctness
• Software verification with PDR: an implementation of the state of the art
• Computer Aided Verification
• Concurrent program verification with invariant-guided underapproximation

Cites work

• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1982207 (Why is no real title available?)
• scientific article; zbMATH DE number 1744961 (Why is no real title available?)
• scientific article; zbMATH DE number 1903353 (Why is no real title available?)
• Abstractions from proofs
• Computer aided verification. 24th international conference, CAV 2012, Berkeley, CA, USA, July 7--13, 2012. Proceedings
• Formalizing the LLVM intermediate representation for verified program transformations
• Guarded commands, nondeterminacy and formal derivation of programs
• LCTD: test-guided proofs for C programs on LLVM
• Lazy abstraction
• Loop summarization using state and transition invariants
• SAT-Based Model Checking without Unrolling
• Software Model Checking: Searching for Computations in the Abstract or the Concrete
• Software model checking
• Thread-modular abstraction refinement.
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(1)

• LCTD: test-guided proofs for C programs on LLVM

Describes a project that uses

Uses Software

• Boolector
• CUTE
• z3
• LLVM
• KLEE
• DART
• Predator
• CPAchecker
• CBMC
• Threader
• YOGI
• Vellvm
• LCTD
• BoogiePL
• SMACK
• jCUTE
• LCT
• STP

This page was built for publication: LCTD: test-guided proofs for C programs on LLVM

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q338629)