A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
From MaRDI portal
Recommendations
- A linear algebraic approach to Datalog evaluation
- Datalog LITE
- scientific article; zbMATH DE number 1696847
- Linearisability on Datalog programs
- Solving quantified verification conditions using satisfiability modulo theories
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Bottom-up evaluation of Datalog programs with arithmetic constraints
- A practical approach to satisfiability modulo linear integer arithmetic
- A new technique for verifying and correcting logic programs
- A verified proof checker for higher-order logic
Cites work
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
- Applying Linear Quantifier Elimination
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Complete problems in the first-order predicate calculus
- Complexity and related enhancements for automated theorem-proving programs
- Complexity results for classes of quantificational formulas
- Computing small clause normal forms
- Deciding the Bernays-Schoenfinkel fragment over bounded difference constraints by simple clause learning over theories
- Efficient model construction for Horn logic with VLog (system description)
- Faster, higher, stronger: E 2.3
- Hierarchic superposition revisited
- Horn clause solvers for program verification
- Isabelle/HOL. A proof assistant for higher-order logic
- On the combination of the Bernays-Schönfinkel-Ramsey fragment with simple linear integer arithmetic
- On the verification of security-aware E-services
- Refutational theorem proving for hierarchic first-order theories
- Revisiting enumerative instantiation
- SCL clause learning from simple models
- SPASS-SATT. A CDCL(LA) solver
- Sledgehammer: judgement day
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Superposition for bounded domains
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- Universal invariant checking of parametric systems with quantifier-free SMT reasoning
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Cited in
(3)
Describes a project that uses
Uses Software
This page was built for publication: A Datalog hammer for supervisor verification conditions modulo simple linear arithmetic
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q831915)
