Lingva: generating and proving program properties using symbol elimination

DOI10.1007/978-3-662-46823-4_6MaRDI QIDQ3455056zbMATH OpenOpenAlexFDO

Authors Laura Kovács

Publication date 3 December 2015

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-46823-4_6

Mathematics Subject Classification ID

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

Recommendations

• A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
• Elimination Techniques for Program Analysis
• Ilinva: using abduction to generate loop invariants
• Reasoning about loops using Vampire in KeY
• Valigator: A Verification Tool with Bound and Invariant Generation

Cites work

• A parametric segmentation functor for fully automatic and scalable array content analysis
• Fluid updates: beyond strong vs. weak updates
• Lazy abstraction with interpolants for arrays
• Quantified Invariant Generation Using an Interpolating Saturation Prover
• SMT-based array invariant generation
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0

Cited in

(2)

• A First Class Boolean Sort in First-Order Theorem Proving and TPTP
• Lingva

Describes a project that uses

Uses Software

• FunArray
• InvGen
• LLVM
• TPTP
• VAMPIRE

This page was built for publication: Lingva: generating and proving program properties using symbol elimination

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