LCTD: test-guided proofs for C programs on LLVM

DOI10.1016/j.jlamp.2015.10.010zbMath1392.68149OpenAlexW2217390717WikidataQ113870959 ScholiaQ113870959MaRDI QIDQ338629

Keijo Heljanko, Olli Saarikivi

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)

Related Items

LCTD: test-guided proofs for C programs on LLVM

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• LCTD: test-guided proofs for C programs on LLVM
• Computer aided verification. 24th international conference, CAV 2012, Berkeley, CA, USA, July 7--13, 2012. Proceedings
• Loop summarization using state and transition invariants
• Formalizing the LLVM intermediate representation for verified program transformations
• SAT-Based Model Checking without Unrolling
• Abstractions from proofs
• Guarded commands, nondeterminacy and formal derivation of programs
• Lazy abstraction
• Software model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Software Model Checking: Searching for Computations in the Abstract or the Concrete
• Computer Aided Verification