Certified Reasoning with Infinity

DOI10.1007/978-3-319-19249-9_31zbMath1427.68054OpenAlexW2293472070MaRDI QIDQ5206958

Andreea Costea, Wei-Ngan Chin, Asankhaya Sharma, Shengyi Wang, Aquinas Hobor

Publication date: 19 December 2019

Published in: FM 2015: Formal Methods (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-19249-9_31

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (1)

Omega++

Uses Software

• Coq
• Isabelle/HOL
• HIP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Quantifier elimination for real algebra -- the quadratic case and beyond
• Isabelle/HOL. A proof assistant for higher-order logic
• Applying Linear Quantifier Elimination
• Interacting with Modal Logics in the Coq Proof Assistant
• Linear Arithmetic with Stars
• Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic
• Effective Quantifier Elimination for Presburger Arithmetic with Infinity
• Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants
• BI as an assertion language for mutable data structures
• Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
• Automated Deduction – CADE-20
• Decision Procedures for Multisets with Cardinality Constraints
• Computer Aided Verification

This page was built for publication: Certified Reasoning with Infinity