LCTD: test-guided proofs for C programs on LLVM

DOI10.1016/J.JLAMP.2015.10.010zbMATH Open1392.68149OpenAlexW2217390717WikidataQ113870959 ScholiaQ113870959MaRDI QIDQ338629FDOQ338629

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

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

zbMATH Keywords

verificationabstraction refinementautomated testingdynamic symbolic executionpredicate abstractionweakest precondition

Mathematics Subject Classification ID

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

Cites Work

• Formalizing the LLVM intermediate representation for verified program transformations
• Title not available (Why is that?)
• SAT-Based Model Checking without Unrolling
• Abstractions from proofs
• Guarded commands, nondeterminacy and formal derivation of programs
• Loop summarization using state and transition invariants
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Thread-modular abstraction refinement.

Cited In (1)

• 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

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)