Lingva: Generating and Proving Program Properties Using Symbol Elimination

DOI10.1007/978-3-662-46823-4_6zbMath1434.68106OpenAlexW2295411989MaRDI QIDQ3455056

Unnamed Author, 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)

Related Items

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

Uses Software

• VAMPIRE
• TPTP
• LLVM
• InvGen
• FunArray

Cites Work

• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Lazy Abstraction with Interpolants for Arrays
• SMT-Based Array Invariant Generation
• Fluid Updates: Beyond Strong vs. Weak Updates
• A parametric segmentation functor for fully automatic and scalable array content analysis
• Quantified Invariant Generation Using an Interpolating Saturation Prover