BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
theorem proving
Google theorem proving

Tag #theorem proving

404 papers:

IFM-2019-KringsL #constraints #interactive #proving
Embedding SMT-LIB into B for Interactive Proof and Constraint Solving (SK, ML), pp. 265–283.
HaskellHaskell-2019-HallahanXP #constraints #haskell #named
G2Q: Haskell constraint solving (WTH, AX, RP), pp. 44–57.
ICMLICML-2019-BansalLRSW #higher-order #logic #machine learning #named #proving
HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving (KB, SML, MNR, CS, SW), pp. 454–463.
PADLPADL-2019-Tarau #combinator #framework #proving #testing
A Combinatorial Testing Framework for Intuitionistic Propositional Theorem Provers (PT), pp. 115–132.
PPDPPPDP-2019-Kikuchi0S #induction #program transformation #proving #term rewriting
Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation (KK, TA0, IS), p. 14.
CADECADE-2019-LiT #automation #protocol #proving #security #verification
Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (DLL, AT), pp. 354–365.
SEFMSEFM-2018-DuboisGPC #interactive #protocol #proving #using
Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem Prover (CD, OG, JP, MC), pp. 239–253.
HaskellHaskell-2018-VazouBKHH #equation #functional #haskell #proving #reasoning
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl) (NV, JB, RK, DVH, GH), pp. 132–144.
PPDPPPDP-2018-GreweEPM #automation #framework #proving
System Description: An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers (SG, SE, AP, MM), p. 10.
ICSMEICSME-2017-Shi #algorithm #constraints #optimisation
Combining Evolutionary Algorithms with Constraint Solving for Configuration Optimization (KS), pp. 665–669.
FDGFDG-2017-KarthS #constraints
WaveFunctionCollapse is constraint solving in the wild (IK, AMS), p. 10.
ICSE-2017-ThomeSBB #constraints #detection #string
Search-driven string constraint solving for vulnerability detection (JT, LKS, DB, LCB), pp. 198–208.
CADECADE-2017-HustadtOD #logic #metric #proving
Theorem Proving for Metric Temporal Logic over the Naturals (UH, AO, CD), pp. 326–343.
CADECADE-2017-ItegulovSP #proving
Scavenger 0.1: A Theorem Prover Based on Conflict Resolution (DI, JS, BWP), pp. 344–356.
CADECADE-2017-MengRTB #constraints #relational #smt
Relational Constraint Solving in SMT (BM, AR, CT, CWB), pp. 148–165.
TAPTAP-2017-Reger0V #case study #challenge #experience #proving #testing
Testing a Saturation-Based Theorem Prover: Experiences and Challenges (GR, MS0, AV), pp. 152–161.
ASEASE-2016-LiLQHBYCL #constraints #execution #machine learning #symbolic computation
Symbolic execution of complex program driven by machine learning based constraint solving (XL, YL, HQ, YQH, LB, YY, XC, XL), pp. 554–559.
ESOPESOP-2016-MineBR #algorithm #constraints #induction #invariant #source code
An Algorithm Inspired by Constraint Solvers to Infer Inductive Invariants in Numeric Programs (AM, JB, TWR), pp. 560–588.
ICTSSICTSS-2016-PetrenkoNR #automaton #constraints #generative #testing
Test Generation by Constraint Solving and FSM Mutant Killing (AP, ONT, SR), pp. 36–51.
IJCARIJCAR-2016-BrombergerW #constraints #performance #testing
Fast Cube Tests for LIA Constraint Solving (MB, CW), pp. 116–132.
IJCARIJCAR-2016-SchulzM #heuristic #performance #proving
Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (SS0, MM), pp. 330–345.
HaskellHaskell-2015-Gundry #constraints #haskell #plugin
A typechecker plugin for units of measure: domain-specific constraint solving in GHC Haskell (AG), pp. 11–22.
OOPSLAOOPSLA-2015-FelgentreffMBH #constraints #programming language
Checks and balances: constraint solving without surprises in object-constraint programming languages (TF, TDM, AB, RH), pp. 767–782.
ICSEICSE-v1-2015-HenardPHT #configuration management #constraints #multi #product line #scalability
Combining Multi-Objective Search and Constraint Solving for Configuring Large Software Product Lines (CH, MP, MH, YLT), pp. 517–528.
ICSEICSE-v1-2015-MilicevicNKJ #constraints #higher-order #relational
Alloy*: A General-Purpose Higher-Order Relational Constraint Solver (AM, JPN, EK, DJ), pp. 609–619.
CADECADE-2015-BackemanR #bound #proving
Theorem Proving with Bounded Rigid E-Unification (PB, PR), pp. 572–587.
CADECADE-2015-Baumgartner #named #proving
SMTtoTPTP — A Converter for Theorem Proving Formats (PB), pp. 285–294.
CADECADE-2015-BaumgartnerBW #named #proving
Beagle — A Hierarchic Superposition Theorem Prover (PB, JB, UW), pp. 367–377.
CADECADE-2015-FultonMQVP #axiom #hybrid #proving
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (NF, SM, JDQ, MV, AP), pp. 527–538.
CADECADE-2015-HouGT #automation #logic #proving
Automated Theorem Proving for Assertions in Separation Logic with All Connectives (ZH, RG, AT), pp. 501–516.
CADECADE-2015-MouraKADR #agile #proving
The Lean Theorem Prover (LMdM, SK, JA, FvD, JvR), pp. 378–388.
ISSTAISSTA-2015-KhoshnoodKW #concurrent #constraints #debugging #named
ConcBugAssist: constraint solving for diagnosis and repair of concurrency bugs (SK, MK, CW), pp. 165–176.
HOFMHOFM-2014-BeckertGB #evaluation #interactive #proving #usability #using
A Usability Evaluation of Interactive Theorem Provers Using Focus Groups (BB, SG, FB), pp. 3–19.
IFMIFM-2014-BrideKP #constraints #specification #using #verification #workflow
Verifying Modal Workflow Specifications Using Constraint Solving (HB, OK, FP), pp. 171–186.
IFMIFM-2014-ChaudhariD #automation #proving
Automated Theorem Prover Assisted Program Calculations (DLC, OPD), pp. 205–220.
SPLCSPLC-2014-ThumMBHRS #model checking #product line #proving
Potential synergies of theorem proving and model checking for software product lines (TT, JM, FB, MH, AvR, GS), pp. 177–186.
PADLPADL-2014-CampeottoPDFP #constraints #using
Exploring the Use of GPUs in Constraint Solving (FC, ADP, AD, FF, EP), pp. 152–167.
ASEASE-2014-KauslerS #constraints #evaluation #execution #string #symbolic computation
Evaluation of string constraint solvers in the context of symbolic execution (SK, ES), pp. 259–270.
SACSAC-2014-AmadiniGM #constraints
An enhanced features extractor for a portfolio of constraint solvers (RA, MG, JM), pp. 1357–1359.
CAVCAV-2014-Voronkov #architecture #first-order #named #proving
AVATAR: The Architecture for First-Order Theorem Provers (AV), pp. 696–710.
ICLPICLP-J-2014-AmadiniGM #approach #constraints #lazy evaluation #named
SUNNY: a Lazy Portfolio Approach for Constraint Solving (RA, MG, JM), pp. 509–524.
IJCARIJCAR-2014-BaumgartnerBW #finite #proving #quantifier
Finite Quantification in Hierarchic Theorem Proving (PB, JB, UW), pp. 152–167.
IJCARIJCAR-2014-BeyersdorffC #complexity #proving
The Complexity of Theorem Proving in Circumscription and Minimal Entailment (OB, LC), pp. 403–417.
IJCARIJCAR-2014-GoreTW #logic #proving #using
A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description (RG, JT, JW), pp. 262–268.
TAPTAP-2014-KurthSW #constraints #generative #interface #process #testing #uml #using
Generating Test Data from a UML Activity Using the AMPL Interface for Constraint Solvers (FK, SS, SW), pp. 169–186.
MODELSMoDELS-2013-SongBCC #adaptation #constraints #modelling #runtime #self #using
Self-adaptation with End-User Preferences: Using Run-Time Models and Constraint Solving (HS, SB, AC, SC), pp. 555–571.
POPLPOPL-2013-ParkSP #proving
A theorem prover for Boolean BI (JP, JS, SP), pp. 219–232.
DACDAC-2013-WuH #constraints #framework #multi #random #robust #set #verification
A robust constraint solving framework for multiple constraint sets in constrained random verification (BHW, CY(H), p. 7.
CADECADE-2013-HawblitzelKLR #automation #proving #source code #towards #using
Towards Modularly Comparing Programs Using Automated Theorem Provers (CH, MK, SKL, HR), pp. 282–299.
CAVCAV-2013-KovacsV #first-order #proving
First-Order Theorem Proving and Vampire (LK, AV), pp. 1–35.
ICSTSAT-2013-Beyersdorff #complexity #logic #proving
The Complexity of Theorem Proving in Autoepistemic Logic (OB), pp. 365–376.
VMCAIVMCAI-2013-PelleauMTB #abstract domain #constraints
A Constraint Solver Based on Abstract Domains (MP, AM, CT, FB), pp. 434–454.
ICSMEICSM-2012-RupakhetiH #constraints #fault #modelling #similarity #using
Finding errors from reverse-engineered equality models using a constraint solver (CRR, DH), pp. 77–86.
FMFM-2012-CarlierDG #constraints #finite
A Certified Constraint Solver over Finite Domains (MC, CD, AG), pp. 116–131.
FLOPSFLOPS-2012-CastineirasS #constraints #performance
Improving the Performance of FD Constraint Solving in a CFLP System (IC, FSP), pp. 88–103.
FLOPSFLOPS-2012-Triska #constraints #finite #prolog
The Finite Domain Constraint Solver of SWI-Prolog (MT), pp. 307–316.
ICFPICFP-2012-StewartBA #proving
Verified heap theorem prover by paramodulation (GS, LB, AWA), pp. 3–14.
POPLPOPL-2012-Moore #proving
Meta-level features in an industrial-strength theorem prover (JSM), pp. 425–426.
ICSEICSE-2012-BalasubramaniamJKMN #approach #automation #constraints #generative #performance
An automated approach to generating efficient constraint solvers (DB, CJ, LK, IM, PN), pp. 661–671.
ICSEICSE-2012-SamirniSAMTH #automation #constraints #fault #generative #html #php #string #using
Automated repair of HTML generation errors in PHP applications using string constraint solving (HS, MS, SA, TDM, FT, LJH), pp. 277–287.
CAVCAV-2012-BodikT #constraints #source code
Synthesizing Programs with Constraint Solvers (RB, ET), p. 3.
ICSTICST-2012-SiddiquiMK #analysis #constraints #data flow #lightweight
Lightweight Data-Flow Analysis for Execution-Driven Constraint Solving (JHS, DM, SK), pp. 91–100.
ICSTICST-2012-VorobyovK #automation #constraints #generative #static analysis #testing
Combining Static Analysis and Constraint Solving for Automatic Test Case Generation (KV, PK), pp. 915–920.
IJCARIJCAR-2012-JacquelBDD #automation #deduction #modulo theories #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.
LICSLICS-2012-TraytelPB #category theory #composition #data type #higher-order #logic #proving
Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (DT, AP, JCB), pp. 596–605.
ICSTSAT-2012-ZhangMZ #constraints #identification #interactive #optimisation
Faulty Interaction Identification via Constraint Solving and Optimization (JZ, FM, ZZ), pp. 186–199.
WICSAWICSA-2011-BalasubramaniamSJKMN #approach #architecture #constraints #generative #named #performance
Dominion: An Architecture-Driven Approach to Generating Efficient Constraint Solvers (DB, LdS, CJ, LK, IM, PN), pp. 228–231.
SEFMSEFM-2011-ErnstSR #analysis #empirical #interactive #proving #verification
Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving (GE, GS, WR), pp. 188–203.
SEFMSEFM-2011-JacquelBDD #automation #proving #using #verification
Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving (MJ, KB, DD, CD), pp. 253–268.
PLDIPLDI-2011-PerezR #calculus #logic #proving
Separation logic + superposition calculus = heap theorem prover (JANP, AR), pp. 556–566.
TACASTACAS-2011-ChamarthiDMV #proving
The ACL2 Sedan Theorem Proving System (HRC, PCD, PM, DV), pp. 291–295.
CADECADE-2011-AspertiRCT #interactive #proving
The Matita Interactive Theorem Prover (AA, WR, CSC, ET), pp. 64–69.
CADECADE-2011-Brown #higher-order #problem #proving #satisfiability #sequence
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems (CEB), pp. 147–161.
CADECADE-2011-SchneiderS #automation #first-order #ontology #owl #proving #reasoning #using
Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving (MS, GS), pp. 461–475.
ICSTICST-2011-KhalekK #constraints #database #relational #testing #using
Systematic Testing of Database Engines Using a Relational Constraint Solver (SAK, SK), pp. 50–59.
ICGTICGT-2010-OrejasL #constraints #graph transformation
Delaying Constraint Solving in Symbolic Graph Transformation (FO, LL), pp. 43–58.
KEODKEOD-2010-KatsumiG #lifecycle #ontology #proving
Theorem Proving in the Ontology Lifecycle (MK, MG), pp. 37–49.
SEKESEKE-2010-FuL #constraints #detection #string #web
A String Constraint Solver for Detecting Web Application Vulnerability (XF, CCL), pp. 535–542.
ECMFAECMFA-2010-KleinerFA #automation #constraints #formal method #platform
Model Search: Formalizing and Automating Constraint Solving in MDE Platforms (MK, MDDF, PA), pp. 173–188.
PPDPPPDP-2010-Bonacina #on the #proving
On theorem proving for program checking: historical perspective and recent developments (MPB), pp. 1–12.
RERE-2010-SalinesiMDD #constraints #integer #requirements #reuse #using
Using Integer Constraint Solving in Reuse Based Requirements Engineering (CS, RM, DD, OD), pp. 243–251.
ICSEICSE-2010-Ma #analysis #constraints #testing
Constraint solving techniques for software testing and analysis (FM), pp. 417–420.
CAVCAV-2010-Rybalchenko #constraints #theory and practice #verification
Constraint Solving for Program Verification: Theory and Practice by Example (AR), pp. 57–71.
CSLCSL-2010-Rybalchenko #constraints #theory and practice #verification
Constraint Solving for Program Verification: Theory and Practice by Example (AR), p. 51.
ICTSSICTSS-2010-LakhotiaTHH #constraints #execution #float #named #search-based #symbolic computation
FloPSy — Search-Based Floating Point Constraint Solving for Symbolic Execution (KL, NT, MH, JdH), pp. 142–157.
IJCARIJCAR-2010-BaeldeMS #induction #proving
Focused Inductive Theorem Proving (DB, DM, ZS), pp. 278–292.
IJCARIJCAR-2010-KorovinS #named #proving #similarity
iProver-Eq: An Instantiation-Based Theorem Prover with Equality (KK, CS), pp. 196–202.
LICSLICS-2010-Moore #proving #verification
Theorem Proving for Verification: The Early Days (JSM), p. 283.
TAPTAP-2010-Rusu #proving #specification
Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications (VR), pp. 135–150.
ASEASE-2009-SiddiquiMK #constraints #optimisation #performance
Optimizing a Structural Constraint Solver for Efficient Software Checking (JHS, DM, SK), pp. 615–619.
SACSAC-2009-YangLLW #approach #approximate #constraints
An approximate approach to constraint solving in soft sensing (TY, ZL, XL, HW), pp. 1415–1416.
FASEFASE-2009-KovacsV #array #invariant #proving #source code #using
Finding Loop Invariants for Programs over Arrays Using a Theorem Prover (LK, AV), pp. 470–485.
CADECADE-2009-BensaidCP #integer #named #proving
Dei: A Theorem Prover for Terms with Integer Exponents (HB, RC, NP), pp. 146–150.
CADECADE-2009-BonacinaLM #on the #proving #satisfiability
On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving (MPB, CL, LMdM), pp. 35–50.
CADECADE-2009-McLaughlinP #performance #proving
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method (SM, FP), pp. 230–244.
CADECADE-2009-Stickel #proving
Building Theorem Provers (MES), pp. 306–321.
CADECADE-2009-SutcliffeBBT #automation #development #higher-order #logic #proving
Progress in the Development of Automated Theorem Proving for Higher-Order Logic (GS, CB, CEB, FT), pp. 116–130.
CADECADE-2009-SwiderskiPGFS #analysis #dependence #induction #proving #termination
Termination Analysis by Dependency Pairs and Inductive Theorem Proving (SS, MP, JG, CF, PSK), pp. 322–338.
FATESTestCom-FATES-2009-GrieskampQWKC #constraints #interactive #smt
Interaction Coverage Meets Path Coverage by SMT Constraint Solving (WG, XQ, XW, NK, MBC), pp. 97–112.
FATESTestCom-FATES-2009-SubramaniamXGP #approach #proving #testing #using
An Approach for Test Selection for EFSMs Using a Theorem Prover (MS, LX, BG, ZP), pp. 146–162.
VMCAIVMCAI-2009-TalyGT #constraints #logic #using
Synthesizing Switching Logic Using Constraint Solving (AT, SG, AT), pp. 305–319.
SEFMSEFM-2008-GuoS #finite #impact analysis #proving #state machine #using
Formal Change Impact Analyses of Extended Finite State Machines Using a Theorem Prover (BG, MS), pp. 335–344.
FLOPSFLOPS-2008-MellarkodG #constraints #reasoning #set
Integrating Answer Set Reasoning with Constraint Solving Techniques (VSM, MG), pp. 15–31.
ICGTICGT-2008-Pennemann #proving
Resolution-Like Theorem Proving for High-Level Conditions (KHP), pp. 289–304.
PADLPADL-2008-Subbarayan #constraints #performance #reasoning
Efficient Reasoning for Nogoods in Constraint Solvers with BDDs (SS), pp. 53–67.
PLDIPLDI-2008-GulwaniSV #constraints #program analysis
Program analysis as constraint solving (SG, SS, RV), pp. 281–292.
ASEASE-2008-KhalekELK #constraints #generative #relational #testing #using
Query-Aware Test Generation Using a Relational Constraint Solver (SAK, BE, YOL, SK), pp. 238–247.
SACSAC-2008-AbedMS #analysis #graph #multi #proving #reachability #using
Reachability analysis using multiway decision graphs in the HOL theorem prover (SA, OAM, GAS), pp. 333–338.
GPCEGPCE-2008-ZhangAN #constraints #optimisation
From generic to specific: off-line optimization for a general constraint solver (YZ, TA, FN), pp. 45–54.
CAVCAV-2008-Harrison #proving #verification
Theorem Proving for Verification (JH), pp. 11–18.
ICLPICLP-2008-NearBF #declarative #first-order #logic #named #proving
αleanTAP: A Declarative Theorem Prover for First-Order Classical Logic (JPN, WEB, DPF), pp. 238–252.
ICLPICLP-2008-Triska #constraints #finite
Generalising Constraint Solving over Finite Domains (MT), pp. 820–821.
IJCARIJCAR-2008-BenzmullerPTF #automation #higher-order #logic #named #proving
LEO-II — A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (CB, LCP, FT, AF), pp. 162–170.
IJCARIJCAR-2008-Gacek #interactive #proving
The Abella Interactive Theorem Prover (AG), pp. 154–161.
IJCARIJCAR-2008-Korovin #first-order #logic #named #proving
iProver — An Instantiation-Based Theorem Prover for First-Order Logic (KK), pp. 292–298.
IJCARIJCAR-2008-Otten #agile #logic #performance #proving
leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (JO), pp. 283–291.
IJCARIJCAR-2008-PlatzerQ #hybrid #named #proving
KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (AP, JDQ), pp. 171–178.
LISPILC-2007-Frank #constraints #lisp
Constraint solving in common Lisp (SF), p. 10.
LOPSTRLOPSTR-2007-AbdennadherS #approach #constraints #generative #rule-based
Generation of Rule-Based Constraint Solvers: Combined Approach (SA, IS), pp. 106–120.
LOPSTRLOPSTR-2007-ZhangN #constraints #scalability #unification #using
A Scalable Inclusion Constraint Solver Using Unification (YZ, FN), pp. 121–137.
SACSAC-2007-DjelloulDF #constraints #finite #first-order #infinity #prolog #towards #unification #using
Toward a first-order extension of Prolog’s unification using CHR: a CHR first-order constraint solver over finite or infinite trees (KD, TBHD, TWF), pp. 58–64.
SACSAC-2007-KunXY #algorithm #constraints #geometry #parallel
Parallel algorithms on geometric constraint solving (KJ, YG, XL, YZ), pp. 778–779.
CADECADE-2007-TiwariG #logic #program analysis #proving #using
Logical Interpretation: Static Program Analysis Using Theorem Proving (AT, SG), pp. 147–166.
VMCAIVMCAI-2007-BouillaguetKWZR #data type #first-order #proving #using #verification
Using First-Order Theorem Provers in the Jahob Data Structure Verification System (CB, VK, TW, KZ, MCR), pp. 74–88.
VMCAIVMCAI-2007-RybalchenkoS #constraints
Constraint Solving for Interpolation (AR, VSS), pp. 346–362.
FMFM-2006-UmenoL #automaton #case study #protocol #proving #safety #using
Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study (SU, NAL), pp. 64–80.
SFMSFM-2006-Harrison #float #proving #using #verification
Floating-Point Verification Using Theorem Proving (JH), pp. 211–242.
SFMSFM-2006-Manolios #proving #refinement
Refinement and Theorem Proving (PM), pp. 176–210.
PADLPADL-2006-BecketBMSSW #constraints
Adding Constraint Solving to Mercury (RB, MJGdlB, KM, ZS, PJS, MW), pp. 118–133.
PADLPADL-2006-HawkinsS #constraints #finite #hybrid #satisfiability
A Hybrid BDD and SAT Finite Domain Constraint Solver (PH, PJS), pp. 103–117.
ASEASE-2006-Jurjens #analysis #automation #java #proving #security #source code #using
Security Analysis of Crypto-based Java Programs using Automated Theorem Provers (JJ), pp. 167–176.
ICSEICSE-2006-ManoliosV #proving #static analysis #termination
Integrating static analysis and general-purpose theorem proving for termination analysis (PM, DV), pp. 873–876.
SACSAC-2006-Kosmatov #constraints #sequence
A constraint solver for sequences and its applications (NK), pp. 404–408.
SACSAC-2006-PavonDL #constraints #geometry #problem
An adjustment model in a geometric constraint solving problem (RP, FD, MVL), pp. 968–973.
SACSAC-2006-ZhangG #composition #constraints #geometry #graph
Spatial geometric constraint solving based on k-connected graph decomposition (GFZ, XSG), pp. 979–983.
CAVCAV-2006-Roe #heuristic #modulo theories #proving #smt
The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover (KR), pp. 467–470.
ISSTAISSTA-2006-YorshBS #abstraction #exclamation #proving #testing
Testing, abstraction, theorem proving: better together! (GY, TB, MS), pp. 145–156.
ICALPICALP-2005-DelzannoG #composition #constraints #process #verification
Compositional Verification of Asynchronous Processes via Constraint Solving (GD, MG), pp. 1239–1250.
ICFPICFP-2005-ChenX #programming #proving
Combining programming with theorem proving (CC, HX), pp. 66–77.
SEKESEKE-2005-LiWMW #constraints #generative #testing
A Constraint Solver for Code-based Test Data Generation (JJL, WEW, XM, DMW), pp. 300–305.
ASEASE-2005-WardKA #framework #named #proving
Prufrock: a framework for constructing polytypic theorem provers (JW, GK, PA), pp. 423–426.
SACSAC-2005-Goualard #algorithm #constraints #on the
On considering an interval constraint solving algorithm as a free-steering nonlinear Gauss-Seidel procedure (FG), pp. 1434–1438.
DATEDATE-2005-IyerPC #constraints #learning #performance
Efficient Conflict-Based Learning in an RTL Circuit Constraint Solver (MKI, GP, KTC), pp. 666–671.
TACASTACAS-2005-IsobeR #csp #proving #refinement
A Generic Theorem Prover of CSP Refinement (YI, MR), pp. 108–123.
TACASTACAS-2005-LeinoMO #proving #quantifier
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover (KRML, MM, XO), pp. 334–348.
CADECADE-2005-CastelliniS #first-order #logic #proving
Proof Planning for First-Order Temporal Logic (CC, AS), pp. 235–249.
CADECADE-2005-ChaudhuriP #first-order #linear #logic #proving
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic (KC, FP), pp. 69–83.
CADECADE-2005-MeierM #multi #proving
System Description: Multi A Multi-strategy Proof Planner (AM, EM), pp. 250–254.
CAVCAV-2005-CookKS #named #proving #verification
Cogent: Accurate Theorem Proving for Program Verification (BC, DK, NS), pp. 296–300.
ICLPICLP-2005-BaseliceBG #constraints #integration #set #towards
Towards an Integration of Answer Set and Constraint Solving (SB, PAB, MG), pp. 52–66.
IFMIFM-2004-EllisI #automation #integration #program analysis #proving
An Integration of Program Analysis and Automated Theorem Proving (BJE, AI), pp. 67–86.
IFMIFM-2004-Melham #functional #model checking #proving
Integrating Model Checking and Theorem Proving in a Reflective Functional Language (TFM), pp. 36–39.
SEFMSEFM-2004-ZhangXW #constraints #execution #generative #symbolic computation #testing #using
Path-Oriented Test Data Generation Using Symbolic Execution and Constraint Solving Techniques (JZ, CX, XW), pp. 242–250.
ICEISICEIS-v1-2004-Augusto #model checking #verification
Model Checking and Theorem Proving-Based Verification of EIS (JCA), p. XXXIII-XXXIV.
LOPSTRLOPSTR-2004-Colon #constraints #imperative #source code #synthesis
Schema-Guided Synthesis of Imperative Programs by Constraint Solving (MC), pp. 166–181.
DACDAC-2004-ParthasarathyICW #constraints #performance
An efficient finite-domain constraint solver for circuits (GP, MKI, KTC, LCW), pp. 212–217.
TACASTACAS-2004-LingerS #analysis #constraints #ml #type inference
Binding-Time Analysis for MetaML via Type Inference and Constraint Solving (NL, TS), pp. 266–279.
TACASTACAS-2004-McMillan #proving
An Interpolating Theorem Prover (KLM), pp. 16–30.
CAVCAV-2004-BallCLZ #abstraction #automation #named #proving #refinement
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement (TB, BC, SKL, LZ), pp. 457–461.
CSLCSL-2004-GanzingerK #equation #proving #reasoning
Integrating Equational Reasoning into Instantiation-Based Theorem Proving (HG, KK), pp. 71–84.
CSLCSL-2004-Lynch #proving
Unsound Theorem Proving (CL), pp. 473–487.
IJCARIJCAR-2004-DenneyFS #automation #proving #using
Using Automated Theorem Provers to Certify Auto-generated Aerospace Software (ED, BF, JS), pp. 198–212.
IJCARIJCAR-2004-WintersteinBG #diagrams #proving
Dr.Doodle: A Diagrammatic Theorem Prover (DW, AB, CAG), pp. 331–335.
SEFMSEFM-2003-DeharbeR #debugging #proving #verification
Light-Weight Theorem Proving for Debugging and Verifying Units of Code (DD, SR), pp. 220–228.
LOPSTRLOPSTR-2003-AbdennadherF #constraints #integration #optimisation #rule-based
Integration and Optimization of Rule-Based Constraint Solvers (SA, TWF), pp. 198–213.
LOPSTRLOPSTR-2003-LehmannL #generative #induction #proving #using
Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce (HL, ML), pp. 1–19.
SACSAC-2003-MonfroyC #component #constraints
Basic Components for Constraint Solver Cooperations (EM, CC), pp. 367–374.
SACSAC-2003-Zoeteweij #constraints #coordination #distributed
Coordination-Based Distributed Constraint Solving in DICE (PZ), pp. 360–366.
DACDAC-2003-ChaiK #constraints #performance #pseudo
A fast pseudo-boolean constraint solver (DC, AK), pp. 830–835.
TACASTACAS-2003-VaziriJ #constraints
Checking Properties of Heap-Manipulating Procedures with a Constraint Solver (MV, DJ), pp. 505–520.
CADECADE-2003-DixonF #named #prototype #proving
IsaPlanner: A Prototype Proof Planner in Isabelle (LD, JDF), pp. 279–283.
CAVCAV-2003-ColonSS #constraints #generative #invariant #linear #using
Linear Invariant Generation Using Non-linear Constraint Solving (MC, SS, HS), pp. 420–432.
CAVCAV-2003-FlanaganJOS #lazy evaluation #proving #using
Theorem Proving Using Lazy Proof Explication (CF, RJ, XO, JBS), pp. 355–367.
FATESFATES-2003-HahnleW #proving #testing #using
Using a Software Testing Technique to Improve Theorem Proving (RH, AW), pp. 30–41.
LICSLICS-2003-Comon-LundhS #constraints #deduction
Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or (HCL, VS), p. 271–?.
LICSLICS-2003-GanzingerK #proving
New Directions in Instantiation-Based Theorem Proving (HG, KK), pp. 55–64.
LOPSTRLOPSTR-2002-AbdennadherR #constraints #logic programming #synthesis #using
Constraint Solver Synthesis Using Tabled Resolution for Constraint Logic Programming (SA, CR), pp. 32–47.
DATEDATE-2002-FerrandiRS #constraints #functional #using #verification
Functional Verification for SystemC Descriptions Using Constraint Solving (FF, MR, DS), pp. 744–751.
TACASTACAS-2002-BouquetLP #constraints #named
CLPS-B — A Constraint Solver for B (FB, BL, FP), pp. 188–204.
CADECADE-2002-Brown #higher-order #proving #set
Solving for Set Variables in Higher-Order Theorem Proving (CEB), pp. 408–422.
CADECADE-2002-MouraRS #bound #infinity #lazy evaluation #model checking #proving
Lazy Theorem Proving for Bounded Model Checking over Infinite Domains (LMdM, HR, MS), pp. 438–455.
ICTSSTestCom-2002-CastanetR #analysis #proving #reachability #testing
Generate Certified Test Cases by Combining Theorem Proving and Reachability Analysis (RC, DR), pp. 249–266.
ICALPICALP-2001-KorovinV #constraints
Knuth-Bendix Constraint Solving Is NP-Complete (KK, AV), pp. 979–992.
IFLIFL-2001-MolEP #functional #proving
Theorem Proving for Functional Programmers (MdM, MCJDvE, MJP), pp. 55–71.
PPDPPPDP-2001-AbdennadherR #confluence #constraints #rule-based #using
Using Confluence to Generate Rule-Based Constraint Solvers (SA, CR), pp. 127–135.
ASEASE-2001-CookIM #higher-order #proving #synthesis
Higher Order Function Synthesis Through Proof Planning (AC, AI, GM), pp. 307–310.
FSEESEC-FSE-2001-EdvardssonK #analysis #constraints #generative #testing
Analysis of the constraint solver in UNA based test data generation (JE, MK), pp. 237–245.
CAVCAV-2001-Bertot #formal method #proving #verification
Formalizing a JVML Verifier for Initialization in a Theorem Prover (YB), pp. 14–24.
ICLPICLP-2001-BandaJMNSH #constraints
Building Constraint Solvers with HAL (MJGdlB, DJ, KM, NN, PJS, CH), pp. 90–104.
IJCARIJCAR-2001-Beeson #higher-order #proving
A Second-Order Theorem Prover Applied to Circumscription (MB), pp. 318–324.
IJCARIJCAR-2001-Happe #proving
The MODPROF Theorem Prover (JH), pp. 459–463.
IJCARIJCAR-2001-HodasT #agile #first-order #implementation #linear #logic #named #proving
lolliCop — A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic (JSH, NT), pp. 670–684.
IJCARIJCAR-2001-LetzS #calculus #named #proving
DCTP — A Disconnection Calculus Theorem Prover — System Abstract (RL, GS), pp. 381–385.
IJCARIJCAR-2001-NieuwenhuisHRV #evaluation #on the #proving
On the Evaluation of Indexing Techniques for Theorem Proving (RN, TH, AR, AV), pp. 257–271.
IJCARIJCAR-2001-Pastre #deduction #knowledge-based #proving
MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction (DP), pp. 685–689.
IJCARIJCAR-2001-SchmittLKN #interactive #proving
JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants (SS, LL, CK, AN), pp. 421–426.
ICSTSAT-2001-McllraithA #proving
Theorem Proving with Structured Theories (Preliminary Report)* (SM, EA), pp. 311–328.
UMLUML-2000-Padawitz #constraints #diagrams #how #proving #state machine #uml
Swinging UML: How to Make Class Diagrams and State Machines Amenable to Constraint Solving and Proving (PP), pp. 162–177.
PADLPADL-2000-Hickey #constraints #named
CLIP: A CLP(Intervals) Dialect for Metalevel Constraint Solving (TJH), pp. 200–214.
POPLPOPL-2000-Hickey #constraints
Analytic Constraint Solving and Interval Arithmetic (TJH), pp. 338–351.
SASSAS-2000-Podelski #constraints #model checking
Model Checking as Constraint Solving (AP), pp. 22–37.
TACASTACAS-2000-BharadwajS #automation #constraints #invariant #named
Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking (RB, SS), pp. 378–394.
CADECADE-2000-AndrewsB #education #higher-order #logic #named #proving #tutorial #using
Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic (PBA, CEB), pp. 511–512.
CADECADE-2000-AndrewsBB #proving #type system
System Description: TPS: A Theorem Proving System for Type Theory (PBA, MB, CEB), pp. 164–169.
CADECADE-2000-Harrison #proving #using #verification
High-Level Verification Using Theorem Proving and Formalized Mathematics (JH), pp. 1–6.
CADECADE-2000-NeculaL #generative #proving
Proof Generation in the Touchstone Theorem Prover (GCN, PL), pp. 25–44.
CADECADE-2000-Seger #float #model checking #proving
Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice (CJHS), p. 235.
CADECADE-2000-Sinz #algebra #automation #proving
System Description: ARA — An Automatic Theorem Prover for Relation Algebras (CS), pp. 177–182.
ICLPCL-2000-HahnleHS #constraints #finite #generative #proving
Moder Generation Theorem Proving with Finite Interval Constraints (RH, RH, YS), pp. 285–299.
ICLPCL-2000-MelisM #multi #proving
Proof Planning with Multiple Strategies (EM, AM), pp. 644–659.
ISSTAISSTA-2000-JacksonV #constraints #debugging
Finding bugs with a constraint solver (DJ, MV), pp. 14–25.
WICSAWICSA-1999-HirschIM #constraints #graph grammar #modelling
Modeling Software Architecutes and Styles with Graph Grammars and Constraint Solving (DH, PI, UM), pp. 127–144.
FMFM-v2-1999-Nadjm-TehraniA #design #modelling #proving
Combining Theorem Proving and Continuous Models in Synchronous Design (SNT, ), pp. 1384–1399.
FLOPSFLOPS-1999-FernandezH #constraints #framework
An Interval Lattice-Based Constraint Solving Framework for Lattices (AJF, PMH), pp. 194–208.
ASEASE-1999-StarkI #automation #imperative #proving #synthesis #towards
Towards Automatic Imperative Program Synthesis Through Proof Planning (JS, AI), pp. 44–51.
FASEFASE-1999-LuthTKK #development #proving #tool support
TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving (CL, HT, K, BKB), pp. 239–243.
TACASTACAS-1999-RusuS #abstraction #on the #proving #safety #static analysis
On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction (VR, ES), pp. 178–192.
TACASTACAS-1999-SpeltE #analysis #database #object-oriented
A Theorem Prover-Based Analysis Tool for Object-Oriented Databases (DS, SE), pp. 375–389.
CADECADE-1999-Artemov #on the #proving #verification
On Explicit Reflection in Theorem Proving and Formal Verification (SNA), pp. 267–281.
CADECADE-1999-FrankeK #automation #communication #distributed #proving
System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving (AF, MK), pp. 217–221.
CADECADE-1999-Hickey #distributed #fault tolerance #proving
Fault-Tolerant Distributed Theorem Proving (JH), pp. 227–231.
CADECADE-1999-HutterB #contest #design #induction #proving
The Design of the CADE-16 Inductive Theorem Prover Contest (DH, AB), pp. 374–377.
CADECADE-1999-JanicicBG #flexibility #framework #integration #proving
A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers (PJ, AB, IG), pp. 127–141.
CADECADE-1999-Nipkow #programming language #proving
Invited Talk: Embedding Programming Languages in Theorem Provers (TN), p. 398.
CADECADE-1999-Voronkov #named #proving
KK: a theorem prover for K (AV), pp. 383–387.
CAVCAV-1999-ManoliosNS #bisimulation #model checking #proving
Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation (PM, KSN, RS), pp. 369–379.
CSLCSL-1999-Howe #interactive #proving #type system #using
Interactive Theorem Proving Using Type Theory (DJH), p. 578.
ICLPICLP-1999-DemoenBHMS #constraints
Herbrand Constraint Solving in HAL (BD, MJGdlB, WH, KM, PJS), pp. 260–274.
CSMRCSMR-1998-JakobiW #automation #database #evaluation #framework #maintenance #named #proving
DBFW: A Simple DataBase FrameWork for the Evaluation and Maintenance of Automated Theorem Prover Data (PJ, AW), pp. 185–188.
ICALPICALP-1998-Lugiez #automaton #induction #proving
A Good Class of Tree Automata and Application to Inductive Theorem Proving (DL), pp. 409–420.
LOPSTRLOPSTR-1998-GabricGS #analysis #constraints #strict
Strictness Analysis as Finite-Domain Constraint Solving (TG, KG, HS), pp. 255–270.
LOPSTRLOPSTR-1998-Richardson #named #proving
Abstract: Proof Planning with Program Schemas (JR), pp. 313–315.
ASEASE-1998-Ledru #identification #proving
Identifying Pre-Conditions with the Z/EVES Theorem Prover (YL), p. 32–?.
SACSAC-1998-ArbabM #constraints #coordination #using
Using coordination for cooperative constraint solving (FA, EM), pp. 139–148.
DACDAC-1998-AagaardJS #evaluation #industrial #proving
Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment (MA, RBJ, CJHS), pp. 538–541.
WRLAWRLA-1998-BorovanskyC #constraints #process #using
Cooperation of constraint solvers: using the new process control facilities of ELAN (PB, CC), pp. 1–20.
CADECADE-1998-BenzmullerK98a #higher-order #proving
System Description: LEO — A Higher-Order Theorem Prover (CB, MK), pp. 139–144.
CADECADE-1998-FleuriotP #analysis #geometry #proving #standard
A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia (JDF, LCP), pp. 3–16.
CADECADE-1998-GorePSV #proving #smarttech
System Description: card TAP: The First Theorem Prover on a Smart Card (RG, JP, AS, HV), pp. 47–50.
CADECADE-1998-RichardsonSG #higher-order #logic #proving
System Description: Proof Planning in Higher-Order Logic with Lambda-Clam (JR, AS, IG), pp. 129–133.
CADECADE-1998-SchurmannP #automation #logic #proving
Automated Theorem Proving in a Simple Meta-Logic for LF (CS, FP), pp. 286–300.
CAVCAV-1998-Camilleri #design #multi #proving
A Role for Theorem Proving in Multi-Processor Design (AJC), pp. 45–48.
CAVCAV-1998-HardinWG #concept #design #proving
Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle (DSH, MW, DAG), pp. 39–44.
CSLCSL-1998-NarendranRV #constraints
RPO Constraint Solving Is in NP (PN, MR, RMV), pp. 385–398.
ISSTAISSTA-1998-GotliebBR #automation #constraints #generative #testing #using
Automatic Test Data Generation Using Constraint Solving Techniques (AG, BB, MR), pp. 53–62.
FMFME-1997-AgerholmF #automation #proving #towards
Towards an Integrated CASE and Theorem Proving Tool for VDM-SL (SA, JF), pp. 278–297.
RTARTA-1997-KuhlerW #data type #equation #induction #proving #specification
Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving (UK, CPW), pp. 38–52.
TLCATLCA-1997-Ruess #calculus #proving
Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving (HR), pp. 319–335.
PPDPPLILP-1997-CarlssonOC #constraints #finite
An Open-Ended Finite Domain Constraint Solver (MC, GO, BC), pp. 191–206.
TACASTACAS-1997-SandnerM #proving #refinement
Theorem Prover Support for the Refinement of Stream Processing Functions (RS, OM), pp. 351–365.
TAPSOFTTAPSOFT-1997-KolyangLMW #development #interface #proving
TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving (K0, CL, TM0, BW), pp. 855–858.
CADECADE-1997-Bonacina #proving
The Clause-Diffusion Theorem Prover Peers-mcd (MPB), pp. 53–56.
CADECADE-1997-DahnGHW #automation #integration #interactive #proving
Integration of Automated and Interactive Theorem Proving in ILP (BID, JG, TH, AW), pp. 57–60.
CADECADE-1997-FeltyH #hybrid #interactive #proving #using
Hybrid Interactive Theorem Proving Using Nuprl and HOL (APF, DJH), pp. 351–365.
CADECADE-1997-HasegawaIOK #bottom-up #proving #set #top-down
Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving (RH, KI, YO, MK), pp. 176–190.
CADECADE-1997-Iwanuma #proving #top-down
Lemma Matching for a PTTP-based Top-down Theorem Prover (KI), pp. 146–160.
CADECADE-1997-LoweD #named #proving
XBarnacle: Making Theorem Provers More Accessible (HL, DD), pp. 404–407.
CADECADE-1997-Slaney #logic #named #proving
Minlog: A Minimal Logic Theorem Prover (JKS), pp. 268–271.
CAVCAV-1997-ChanABN #constraints #model checking
Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints (WC, RJA, PB, DN), pp. 316–327.
ICALPICALP-1996-Ganzinger #proving
Saturation-Based Theorem Proving (HG), pp. 1–3.
FMFME-1996-HavelundS #model checking #protocol #proving #verification
Experiments in Theorem Proving and Model Checking for Protocol Verification (KH, NS), pp. 662–681.
RTARTA-1996-BoudetCM #proving #unification
AC-Complete Unification and its Application to Theorem Proving (AB, EC, CM), pp. 18–32.
RTARTA-1996-HillenbrandBF #on the #performance #proving
On Gaining Efficiency in Completion-Based Theorem Proving (TH, AB, RF), pp. 432–435.
RTARTA-1996-Stuber #integer #proving
Superposition Theorem Proving for Albelian Groups Represented as Integer Modules (JS), pp. 33–47.
PPDPALP-1996-Benhamou #constraints
Heterogeneous Constraint Solving (FB), pp. 62–76.
PPDPPLILP-1996-StuckeyT #constraints #logic programming #modelling #probability #using
Models for Using Stochastic Constraint Solvers in Constraint Logic Programming (PJS, VT), pp. 423–437.
SASSAS-1996-Snelting #constraints #metric #slicing #validation
Combining Slicing and Constraint Solving for Validation of Measurement Software (GS), pp. 332–348.
CADECADE-1996-BeckertHOS #proving
The Tableau-based Theorem Prover 3TAP Version 4.0 (BB, RH, PO, MS), pp. 303–307.
CADECADE-1996-DenzingerS #learning #proving
Learning Domain Knowledge to Improve Theorem Proving (JD, SS), pp. 62–76.
CADECADE-1996-Ganzinger #proving
Saturation-Based Theorem Proving: Past Successes and Future Potential (HG), p. 1.
CADECADE-1996-GanzingerW #monad #proving
Theorem Proving in Cancellative Abelian Monoids (HG, UW), pp. 388–402.
CADECADE-1996-KolbeW #proving #reuse #termination
Termination of Theorem Proving by Reuse (TK, CW), pp. 106–120.
CADECADE-1996-Luz-Filho #logic #proving #specification
Grammar Specification in Categorial Logics and Theorem Proving (SFLF), pp. 703–717.
CADECADE-1996-Martin #proving
Theorem Proving with Group Presentations: Examples and Questions (UM), pp. 358–372.
CADECADE-1996-MelisW #proving
Internal Analogy in Theorem Proving (EM, JW), pp. 92–105.
CADECADE-1996-SchaubBN #named #prolog #proving #reasoning
XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description (TS, SB, PN), pp. 293–297.
CADECADE-1996-Schumann #named #parallel #proving
SiCoTHEO: Simple Competitive Parallel Theorem Provers (JS), pp. 240–244.
CADECADE-1996-Tammet #logic #proving
A Resolution Theorem Prover for Intuitonistic Logic (TT), pp. 2–16.
CADECADE-1996-Wang #geometry #named #proving
GEOTHER: A Geometry Theorem Prover (DW), pp. 166–170.
CAVCAV-1996-ClarkeGZ #algorithm #proving #using #verification
Verifying the SRT Division Algorithm Using Theorem Proving Techniques (EMC, SMG, XZ), pp. 111–122.
CAVCAV-1996-GrafS #invariant #proving #using #verification
Verifying Invariants Using theorem Proving (SG, HS), pp. 196–207.
RTARTA-1995-BaaderS #algebra #constraints #perspective
Combination of Constraint Solving Techniques: An Algebraic POint of View (FB, KUS), pp. 352–366.
RTARTA-1995-Stickel #proving #term rewriting
Term Rewriting in Contemporary Resolution Theorem Proving (MES), p. 101.
PEPMPEPM-1995-RamakrishnanRS #analysis #constraints #framework #logic programming #source code
A Symbolic Constraint Solving Framework for Analysis of Logic Programs (CRR, IVR, RCS), pp. 12–23.
CAVCAV-1995-DingelF #abstraction #infinity #model checking #proving #reasoning #using
Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving (JD, TF), pp. 54–69.
ICLPICLP-1995-ChiuL #constraints #linear #using
Interval Linear Constraint Solving Using the Preconditioned Interval Gauss-Seidel Method (CKC, JHML), pp. 17–31.
ICLPICLP-1995-FormicaMT #database #object-oriented #proving #satisfiability
A Theorem Prover for Checking Satisfiability of Object-Oriented Database Schemas (AF, MM, RT), p. 819.
ICLPICLP-1995-Hasegawa #generative #proving
Model Generation Theorem Provers and Their Applications (RH), p. 7.
LICSLICS-1995-ComonNR #constraints #order
Orderings, AC-Theories and Symbolic Constraint Solving (HC, RN, AR), pp. 375–385.
PPDPPLILP-1994-CodognetD #constraints #performance
clp(B): Combining Simplicity and Efficiency in Boolean Constraint Solving (PC, DD), pp. 244–260.
CADECADE-1994-BeckertP #agile #named #proving
leanTAP: Lean Tableau-Based Theorem Proving (BB, JP), pp. 793–797.
CADECADE-1994-BonacinaM #distributed #proving
Distributed Theorem Proving by Peers (MPB, WM), pp. 841–845.
CADECADE-1994-ChuP #first-order #proving #semantics #using
Semantically Guided First-Order Theorem Proving using Hyper-Linking (HC, DAP), pp. 192–206.
CADECADE-1994-ClarkeZ #problem #proving #symbolic computation
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan (EMC, XZ), pp. 758–763.
CADECADE-1994-FeltyH #proving
Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables (APF, DJH), pp. 605–619.
CADECADE-1994-Plaisted #performance #proving
The Search Efficiency of Theorem Proving Strategies (DAP), pp. 57–71.
CADECADE-1994-Schumann #bottom-up #named #preprocessor #proving #top-down
DELTA — A Bottom-up Preprocessor for Top-Down Theorem Provers — System Abstract (JS), pp. 774–777.
CADECADE-1994-WaalG #logic programming #program analysis #program transformation #proving
The Applicability of Logic Program Analysis and Transformation to Theorem Proving (DAdW, JPG), pp. 207–221.
ICLPICLP-1994-KirchnerR #algebra #constraints
Constraint Solving by Narrowing in Combined Algebraic Domains (HK, CR), pp. 617–631.
ICLPILPS-1994-ChiuL #constraints #logic programming #towards
Towards Practical Interval Constraint Solving in Logic Programming (CKC, JHML), pp. 109–123.
RTARTA-1993-AvenhausD #equation #proving
Distributing Equational Theorem Proving (JA, JD), pp. 62–76.
RTARTA-1993-Bachmair #proving
Rewrite Techniques in Theorem Proving (LB), p. 1.
LOPSTRLOPSTR-1993-MaddenHGB #automation #generative #performance #proving #source code #using
A General Technique for Automatically Generating Efficient Programs Through the Use of Proof Planning (PM, JH, IG, AB), pp. 64–66.
PPDPPLILP-1993-CorsiniMRC #abstract interpretation #bottom-up #constraints #finite #performance #prolog
Efficient Bottom-up Abstract Interpretation of Prolog by Means of Constraint Solving over Symbolic Finite Domains (MMC, KM, AR, BLC), pp. 75–91.
CAVCAV-1993-Hungar #model checking #parallel #process #proving #verification
Combining Model Checking and Theorem Proving to Verify Parallel Processes (HH), pp. 154–165.
ICLPILPS-1993-CodognetD #constraints #using
Boolean Constraint Solving Using clp(FD) (PC, DD), pp. 525–539.
KRKR-1992-Lamarre #proving
A Promenade from Monotonicity to Non-Monotonicity Following a Theorem Prover (PL), pp. 572–580.
PPDPALP-1992-BachmairGW #first-order #proving
Theorem Proving for Hierarchic First-Order Theories (LB, HG, UW), pp. 420–434.
LOPSTRLOPSTR-1992-KraanBB #logic programming #proving #synthesis
Logic Program Synthesis via Proof Planning (IK, DAB, AB), pp. 1–14.
ESOPESOP-1992-Gnaedig #proving #specification
ELIOS-OBJ Theorem Proving in a Specification Language (IG), pp. 182–199.
CADECADE-1992-AstrachanS #proving
Caching and Lemmaizing in Model Elimination Theorem Provers (OLA, MES), pp. 224–238.
CADECADE-1992-Baker-PlummerR #proving
The GAZER Theorem Prover (DBP, AR), pp. 726–730.
CADECADE-1992-BeckertGHK #logic #multi #proving
The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics (BB, SG, RH, WK), pp. 758–760.
CADECADE-1992-Chen #empirical #knowledge-based #proving
Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic (WZC), pp. 552–566.
CADECADE-1992-Chou #geometry #proving
A Geometry Theorem Prover for Macintoshes (SCC), pp. 686–690.
CADECADE-1992-ClarkeZ #named #proving
Analytica — A Theorem Prover in Mathematica (EMC, XZ), pp. 761–765.
CADECADE-1992-Dafa #automation #deduction #proving
A Natural Deduction Automated Theorem Proving System (LD), pp. 668–672.
CADECADE-1992-HasegawaKF #generative #lazy evaluation #named #parallel #proving
MGTP: A Parallel Theorem Prover Based on Lazy Model Generation (RH, MK, HF), pp. 776–780.
CADECADE-1992-InoueKH #generative #proving
Embedding Negation as Failure into a Model Generation Theorem Prover (KI, MK, RH), pp. 400–415.
CADECADE-1992-LuskMS #named #parallel #proving
ROO: A Parallel Theorem Prover (ELL, WM, JKS), pp. 731–734.
CADECADE-1992-NieuwenhuisR #proving
Theorem Proving with Ordering Constrained Clauses (RN, AR), pp. 477–491.
CADECADE-1992-RandellCC #automation #challenge #proving
Computing Transivity Tables: A Challenge For Automated Theorem Provers (DAR, AGC, ZC), pp. 786–790.
CADECADE-1992-Schumann #logic #named #proving
KPROP — An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (JS), pp. 740–742.
CADECADE-1992-Voronkov #logic #proving #standard
Theorem Proving in Non-Standard Logics Based on the Inverse Method (AV), pp. 648–662.
CADECADE-1992-WalshNB #proving #using
The Use of Proof Plans to Sum Series (TW, AN, AB), pp. 325–339.
CAVCAV-1992-WrightL #algorithm #concurrent #proving #reasoning #using
Using a Theorem Prover for Reasoning about Concurrent Algorithms (JvW, TL), pp. 56–68.
ICLPJICSLP-1992-KirchnerR #algebra #algorithm #constraints #finite #unification
A Constraint Solver in Finite Algebras and Its Combination with Unification Algorithms (HK, CR), pp. 225–239.
RTARTA-1991-BonacinaH #on the #proving
On Fairness of Completion-Based Theorem Proving Strategies (MPB, JH), pp. 348–360.
RTARTA-1991-Deruyver #equation #first-order #logic #named #proving
EMMY: A Refutational Theorem Prover for First-Order Logic with Equation (AD), pp. 439–441.
RTARTA-1991-Fraus #proving
A Narrowing-Based Theorem Prover (UF), pp. 435–436.
KRKR-1991-HalpernV #model checking #proving
Model Checking vs. Theorem Proving: A Manifesto (JYH, MYV), pp. 325–334.
OOPSLAOOPSLA-1991-Wilk #constraints #named #object-oriented
Equate: An Object-Oriented Constraint Solver (MRW), pp. 286–298.
PPDPPLILP-1991-FrausH #proving
A Narrowing-Based Theorem Prover (UF, HH), pp. 421–422.
ICLPICLP-1991-FujitaH #algorithm #generative #proving #using
A Model Generation Theorem Prover in KL1 Using a Ramified -Stack Algorithm (HF, RH), pp. 535–548.
ICLPICLP-1991-Hagiya #higher-order #proving #unification
Higher-Order Unification as a Theorem Proving Procedure (MH), pp. 270–284.
PPDPPLILP-1990-Jaakola #algorithm #constraints
Modifying the Simplex Algorithm to a Constraint Solver (JJ), pp. 89–105.
ICSEICSE-1990-LafontaineLS #case study #development #empirical #formal method #proving #using
An Experiment in Formal Software Development: Using the B Theorem Prover on a VDM Case Study (CL, YL, PYS), pp. 34–42.
CADECADE-1990-AndrewsINP #proving
The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 641–642.
CADECADE-1990-BoyerM #logic #proving
A Theorem Prover for a Computational Logic (RSB, JSM), pp. 1–15.
CADECADE-1990-ButlerFJO #parallel #proving
A High-Performance Parallel Theorem Prover (RB, ITF, AJ, RAO), pp. 649–650.
CADECADE-1990-ChouG #algorithm #composition #geometry #proving
Ritt-Wu’s Decomposition Algorithm and Geometry Theorem Proving (SCC, XSG), pp. 207–220.
CADECADE-1990-CostaHLS #automation #implementation #logic #proving
Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation (NCAdC, LJH, JJL, VSS), pp. 72–86.
CADECADE-1990-Gramlich #induction #named #proving
UNICOM: A Refined Completion Based Inductive Theorem Prover (BG), pp. 655–656.
CADECADE-1990-HeiselRS #proving #verification
Tactical Theorem Proving in Program Verification (MH, WR, WS), pp. 117–131.
CADECADE-1990-HsiangJ #proving #tutorial
Tutorial on Rewrite-Based Theorem Proving (JH, JPJ), p. 684.
CADECADE-1990-KaflZ #proving #verification
The Theorem Prover of the Program Verifier Tatzelwurm (TK, NZ), pp. 657–658.
CADECADE-1990-LuskM #automation #proving #tutorial
Tutorial on High-Performance Automated Theorem Proving (ELL, WM), p. 681.
CADECADE-1990-MurrayR #named #proving
DISSOLVER: A Dissolution-based Theorem Prover (NVM, ER), pp. 665–666.
CADECADE-1990-SchumannL #named #parallel #proving
PARTHEO: A High-Performance Parallel Theorem Prover (JS, RL), pp. 40–56.
CADECADE-1990-SchumannLK #implementation #parallel #performance #proving #tutorial
Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation (JS, RL, FJK), p. 683.
CADECADE-1990-Schwind #decidability #logic #proving #set
A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic (CS), pp. 528–542.
CADECADE-1990-Stickel #prolog #proving
A Prolog Technology Theorem Prover (MES), pp. 673–674.
CADECADE-1990-Sutcliffe #proving
A General Clause Theorem Prover (GS), pp. 675–676.
CADECADE-1990-Tuominen #framework #logic #proving
Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic (HT), pp. 514–527.
RTARTA-1989-AvenhausDM #named #performance #proving
THEOPOGLES — An efficient Theorem Prover based on Rewrite-Techniques (JA, JD, JM), pp. 538–541.
RTARTA-1989-BonacinaS #equation #named #proving
KBlab: An Equational Theorem Prover for the Macintosh (MPB, GS), pp. 548–550.
LICSLICS-1989-BoseCLM #horn clause #named #parallel #proving
PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (SB, EMC, DEL, SM), pp. 80–89.
SIGMODSIGMOD-1988-MazumdarSS #proving #security #using
Resolving the Tension between Integrity and Security Using a Theorem Prover (SM, DWS, TS), pp. 233–242.
FMVDME-1988-JonesM #design #empirical #named #proving #user interface
MUFFIN: A User Interface Design Experiment for a Theorem Proving Assistant (CBJ, RCM), pp. 337–375.
CADECADE-1988-AllenBCM #horn clause #named #parallel #proving
PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (PEA, SB, EMC, SM), pp. 764–765.
CADECADE-1988-AndrewsINP #proving
The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 760–761.
CADECADE-1988-BrownP #logic #named #proving
SYMEVAL: A Theorem Prover Based on the Experimental Logic (FMB, SSP), pp. 756–757.
CADECADE-1988-CyrlukHK #algebra #geometry #named #proving
GEOMETER: A Theorem Prover for Algebraic Geometry (DC, RMH, DK), pp. 770–771.
CADECADE-1988-FeltyM #higher-order #logic programming #programming language #proving #specification
Specifying Theorem Provers in a Higher-Order Logic Programming Language (APF, DM), pp. 61–80.
CADECADE-1988-Hines #knowledge-based #proving
Hyper-Chaining and Knowledge-Based Theorem Proving (LMH), pp. 469–486.
CADECADE-1988-Kaufmann #interactive #proving
An Interactive Enhancement to the Boyer-Moore Theorem Prover (MK), pp. 735–736.
CADECADE-1988-MantheyB #named #prolog #proving
SATCHMO: A Theorem Prover Implemented in Prolog (RM, FB), pp. 415–434.
CADECADE-1988-McRobbieMT #automation #knowledge-based #logic #performance #proving #standard #towards
Towards Efficient “Knowledge-Based” Automated Theorem Proving for Non-Standard Logics (MAM, RKM, PBT), pp. 197–217.
CADECADE-1988-Paulson #named #proving
Isabelle: The Next Seven Hundred Theorem Provers (LCP), pp. 772–773.
CADECADE-1988-Plaisted #proving
A Goal Directed Theorem Prover (DAP), p. 737.
CADECADE-1988-Stevens #challenge #problem #proving
Challenge Problems from Nonassociative Rings for Theorem Provers (RLS), pp. 730–734.
CADECADE-1988-Stickel88a #prolog #proving
A Prolog Technology Theorem Prover (MES), pp. 752–753.
CADECADE-1988-ZhangK #first-order #proving #using
First-Order Theorem Proving Using Conditional Rewrite Rules (HZ, DK), pp. 1–20.
LICSLICS-1987-BachmairD #first-order #proving
Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.
LICSLICS-1987-GallierRS #equation #proving #using
Theorem Proving Using Rigid E-Unification Equational Matings (JHG, SR, WS), pp. 338–346.
CADECADE-1986-AbadiM #proving
Modal Theorem Proving (MA, ZM), pp. 172–189.
CADECADE-1986-AndrewsPIK #proving
The TPS Theorem Proving System (PBA, FP, SI, CPK), pp. 663–664.
CADECADE-1986-BeierleOV #automation #proving
Automatic Theorem Proving in the ISDV System (CB, WGO, AV), pp. 670–671.
CADECADE-1986-BiundoHHW #induction #proving
The Karlsruhe Induction Theorem Proving System (SB, BH, DH, CW), pp. 672–674.
CADECADE-1986-ButlerLMO #automation #proving
Paths to High-Performance Automated Theorem Proving (RB, ELL, WM, RAO), pp. 588–597.
CADECADE-1986-Chou #geometry #named #proving
GEO-Prover — A Geometry Theorem Prover Developed at UT (SCC), pp. 679–680.
CADECADE-1986-GreenbaumP #proving
The Illinois Prover: A General Purpose Resolution Theorem Prover (SG, DAP), pp. 685–687.
CADECADE-1986-HsiangR #proving
A New Method for Establishing Refutational Completeness in Theorem Proving (JH, MR), pp. 141–152.
CADECADE-1986-Huet86a #proving
Theorem Proving Systems of the Formel Project (GPH), pp. 687–688.
CADECADE-1986-KutzlerS #algorithm #geometry #proving
A Geometry Theorem Prover Based on Buchberger’s Algorithm (BK, SS), pp. 693–694.
CADECADE-1986-LoganantharajM #graph #parallel #proving
Parallel Theorem Proving with Connection Graphs (RL, RAM), pp. 337–352.
CADECADE-1986-Stickel #compilation #implementation #prolog #proving
A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler (MES), pp. 573–587.
CADECADE-1986-ThistlewaiteMM #automation #proving
The KRIPKE Automated Theorem Proving System (PBT, MAM, RKM), pp. 705–706.
LICSLICS-1986-ChouK #geometry #on the #proving
On Mechanical Theorem Proving in Minkowskian Plane Geometry (SCC, HPK), pp. 187–192.
RTARTA-1985-Hsiang #proving #term rewriting
Two Results in Term Rewriting Theorem Proving (JH), pp. 301–324.
CADECADE-1984-OhlbachW #automation #logic #problem #proving
Solving a Problem in Relevance Logic with an Automated Theorem Prover (HJO, GW), pp. 496–508.
CADECADE-1984-Plaisted #analysis #dependence #graph #proving #using
Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving (DAP), pp. 356–374.
CADECADE-1984-Stickel #case study #commutative #proving
A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity (MES), pp. 248–258.
CADECADE-1984-Suppes #generative #interactive #proving
The Next Generation of Interactive Theorem Provers (PS), pp. 303–315.
ICLPSLP-1984-Stickel84 #prolog #proving
A Prolog Technology Theorem Prover (MES), pp. 211–217.
ICALPICALP-1983-HsiangD #proving
Rewrite Methods for Clausal and Non-Clausal Theorem Proving (JH, ND), pp. 331–346.
ICALPICALP-1980-Turchin #optimisation #proving #using
The Use of Metasystem Transition in Theorem Proving and Program Optimization (VFT), pp. 645–657.
CADECADE-1980-EricksonM #proving #scalability
The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs (RWE, DRM), pp. 220–231.
CADECADE-1980-Gloess #correctness #empirical #parsing #proving
An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions (PYG), pp. 154–169.
CADECADE-1980-Nederpelt #approach #proving #λ-calculus
An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus (RN), pp. 182–194.
CADECADE-1980-Plaisted #abstraction #proving
Abstraction Mappings in Mechanical Theorem Proving (DAP), pp. 264–280.
ICALPICALP-1976-Galil #integer #on the #programming #proving
On Enumeration Procedures for Theorem Proving and for Integer Programming (ZG), pp. 355–381.
STOCSTOC-1970-KingF #integer #proving
An Interpretation Oriented Theorem Prover over Integers (JCK, RWF), pp. 169–179.
STOCSTOC-1970-Reiter #proving
The Predicate Elimination Strategy in Theorem Proving (RR), pp. 180–183.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.