A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
From MaRDI portal
Publication:831915
DOI10.1007/978-3-030-86205-3_1OpenAlexW3202430163MaRDI QIDQ831915
Markus Krötzsch, Christoph Weidenbach, Martin Bromberger, Irina Dragoste, Rasha Faqeh, Christof Fetzer
Publication date: 24 March 2022
Full work available at URL: https://arxiv.org/abs/2107.03189
Related Items (2)
A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic ⋮ An efficient subsumption test pipeline for BS(LRA) clauses
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- On the verification of security-aware E-services
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Complete problems in the first-order predicate calculus
- Complexity results for classes of quantificational formulas
- Complexity and related enhancements for automated theorem-proving programs
- Refutational theorem proving for hierarchic first-order theories
- Isabelle/HOL. A proof assistant for higher-order logic
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Efficient model construction for Horn logic with VLog (system description)
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- Hierarchic superposition revisited
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- SPASS-SATT. A CDCL(LA) solver
- SCL clause learning from simple models
- Faster, higher, stronger: E 2.3
- Revisiting enumerative instantiation
- On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic
- Horn Clause Solvers for Program Verification
- Applying Linear Quantifier Elimination
- Solving SAT and SAT Modulo Theories
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Superposition for Bounded Domains
- Sledgehammer: Judgement Day
This page was built for publication: A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
