Tag #modulo theories
43 papers:
- FSCD-2019-BlanquiGH #dependence #dependent type #termination #type system
- Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting (FB, GG, OH), p. 21.
- CAV-2018-AbateDKKP #induction #synthesis
- Counterexample Guided Inductive Synthesis Modulo Theories (AA, CD, PK, DK, EP), pp. 270–288.
- IJCAR-2018-EchenimPS #framework #generative
- A Generic Framework for Implicate Generation Modulo Theories (ME, NP, YS), pp. 279–294.
- IJCAR-2018-FazekasBB #algorithm #satisfiability #set
- Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (KF, FB, AB), pp. 134–151.
- CADE-2017-BonacinaGS #satisfiability
- Satisfiability Modulo Theories and Assignments (MPB, SGL, NS), pp. 42–59.
- PLDI-2016-KentKT #type system
- Occurrence typing modulo theories (AMK, DK0, STH), pp. 296–309.
- CAV-2016-NiemetzPB #precise #satisfiability
- Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories (AN, MP, AB), pp. 199–217.
- TACAS-2015-SebastianiT #cost analysis #optimisation
- Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions (RS, PT), pp. 335–349.
- CAV-2015-DietschHLP #approach #ltl #model checking
- Fairness Modulo Theory: A New Approach to LTL Software Model Checking (DD, MH, VL, AP), pp. 49–66.
- CAV-2015-SebastianiT #named #optimisation
- OptiMathSAT: A Tool for Optimization Modulo Theories (RS, PT), pp. 447–454.
- CAV-2015-ManoliosPP #framework #programming
- The Inez Mathematical Programming Modulo Theories Framework (PM, JP, VP), pp. 53–69.
- ICLP-J-2015-AlvianoP #fuzzy #satisfiability #set
- Fuzzy answer set computation via satisfiability modulo theories (MA, RP), pp. 588–603.
- LCTES-2014-HenryAMM #encoding #execution #how #optimisation #semantics #worst-case
- How to compute worst-case execution time by optimization modulo theory and a clever encoding of program semantics (JH, MA, DM, CM), pp. 43–52.
- TACAS-2014-CimattiGMT #abstraction
- IC3 Modulo Theories via Implicit Predicate Abstraction (AC, AG, SM, ST), pp. 46–61.
- TACAS-2014-DeckerLT #monitoring
- Monitoring Modulo Theories (ND, ML, DT), pp. 341–356.
- HILT-2013-Bjorner #development #satisfiability
- Satisfiability modulo theories for high integrity development (NB), pp. 5–6.
- CAV-2013-ManoliosP
- ILP Modulo Theories (PM, VP), pp. 662–677.
- SAT-2013-CimattiGSS #approach #composition #satisfiability
- A Modular Approach to MaxSAT Modulo Theories (AC, AG, BJS, RS), pp. 150–165.
- CAV-2012-LalQL #reachability
- A Solver for Reachability Modulo Theories (AL, SQ, SKL), pp. 427–443.
- IJCAR-2012-JacquelBDD #automation #deduction #proving #theorem proving #using #verification
- Tableaux Modulo Theories Using Superdeduction — An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover (MJ, KB, DD, CD), pp. 332–338.
- SMT-2012-AlbertiBGRS #library #reachability
- Reachability Modulo Theory Library (FA, RB, SG, SR, NS), pp. 67–76.
- SMT-2012-BjornerMR #satisfiability #verification
- Program Verification as Satisfiability Modulo Theories (NB, KLM, AR), pp. 3–11.
- TACAS-2011-ConchonCI
- Canonized Rewriting and Ground AC Completion Modulo Shostak Theories (SC, EC, MI), pp. 45–59.
- VMCAI-2011-SuterSK #constraints #satisfiability #set
- Sets with Cardinality Constraints in Satisfiability Modulo Theories (PS, RS, VK), pp. 403–418.
- CSL-2010-Strub #coq
- Coq Modulo Theory (PYS), pp. 529–543.
- IJCAR-2010-GhilardiR #model checking #named
- MCMT: A Model Checker Modulo Theories (SG, SR), pp. 22–29.
- DATE-2009-KinsmanN #finite #precise #using
- Finite Precision bit-width allocation using SAT-Modulo Theory (ABK, NN), pp. 1106–1111.
- CAV-2009-GeM #quantifier #satisfiability
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories (YG, LMdM), pp. 306–320.
- SAT-2009-KimSJ #performance #satisfiability
- Efficient Term-ITE Conversion for Satisfiability Modulo Theories (HK, FS, HJ), pp. 195–208.
- SAT-2009-Nieuwenhuis #algorithm #satisfiability
- SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms (RN), p. 1.
- TACAS-2008-CimattiGS #generative #performance #satisfiability
- Efficient Interpolant Generation in Satisfiability Modulo Theories (AC, AG, RS), pp. 397–412.
- RTA-2007-NieuwenhuisORR #challenge #satisfiability
- Challenges in Satisfiability Modulo Theories (RN, AO, ERC, AR), pp. 2–18.
- CADE-2007-GeBT #quantifier #satisfiability #using #verification
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories (YG, CB, CT), pp. 167–182.
- CAV-2007-MouraDS #satisfiability #tutorial
- A Tutorial on Satisfiability Modulo Theories (LMdM, BD, NS), pp. 20–36.
- SAT-2007-CimattiGS #flexibility #satisfiability
- A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories (AC, AG, RS), pp. 334–339.
- CAV-2006-Roe #heuristic #proving #smt #theorem proving
- The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover (KR), pp. 467–470.
- SAT-2006-NieuwenhuisO #on the #optimisation #problem #satisfiability
- On SAT Modulo Theories and Optimization Problems (RN, AO), pp. 156–169.
- SAT-2006-SheiniS #satisfiability
- From Propositional Satisfiability to Satisfiability Modulo Theories (HMS, KAS), pp. 1–9.
- SAT-2006-SheiniS06a #satisfiability
- A Progressive Simplifier for Satisfiability Modulo Theories (HMS, KAS), pp. 184–197.
- RTA-2005-DowekW
- Arithmetic as a Theory Modulo (GD, BW), pp. 423–437.
- CAV-2005-BarrettMS #contest #named #satisfiability
- SMT-COMP: Satisfiability Modulo Theories Competition (CWB, LMdM, AS), pp. 20–23.
- CAV-2005-BozzanoBCJRRS #performance #satisfiability
- Efficient Satisfiability Modulo Theories via Delayed Theory Combination (MB, RB, AC, TAJ, SR, PvR, RS), pp. 335–349.
- TLCA-2001-Dowek
- The Stratified Foundations as a Theory Modulo (GD), pp. 136–150.