Stem prove$ (all stems)

435 papers:

DATE-2015-DarkeCVSM #approximate #bound #model checking #using

Over-approximating loops to prove properties using bounded model checking (PD, BC, RV, US, RM), pp. 1407–1412.

FM-2015-KroeningLW #automaton #bound #model checking #proving #safety

Proving Safety with Trace Automata and Bounded Model Checking (DK, ML, GW), pp. 325–341.

ICGT-2015-Bruggink0NZ #graph #graph transformation #proving #termination #using

Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings (HJSB, BK, DN, HZ), pp. 52–68.

SOSP-2015-HawblitzelHKLPR #distributed #named #proving

IronFleet: proving practical distributed systems correct (CH, JH, MK, JRL, BP, MLR, STVS, BZ), pp. 1–17.

CADE-2015-BackemanR #bound #proving #theorem proving

Theorem Proving with Bounded Rigid E-Unification (PB, PR), pp. 572–587.

CADE-2015-Baumgartner #named #proving #theorem proving

SMTtoTPTP — A Converter for Theorem Proving Formats (PB), pp. 285–294.

CADE-2015-HouGT #automation #logic #proving #theorem proving

Automated Theorem Proving for Assertions in Separation Logic with All Connectives (ZH, RG, AT), pp. 501–516.

CADE-2015-MaricJM #correctness #higher-order #proving #using

Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 (FM, PJ, MM), pp. 256–271.

CAV-2015-KarbyshevBIRS #invariant #proving

Property-Directed Inference of Universal Invariants or Proving Their Absence (AK, NB, SI, NR, SS), pp. 583–602.

ICLP-J-2015-AngelisFPP #correctness #horn clause #imperative #proving #source code

Proving correctness of imperative programs by linearizing constrained Horn clauses (EDA, FF, AP, MP), pp. 635–650.

RTA-2015-EndrullisZ #automaton #finite #proving

Proving non-termination by finite automata (JE, HZ), pp. 160–176.

VMCAI-2015-ChristakisG #composition #image #memory management #parsing #proving #safety #testing #using

Proving Memory Safety of the ANI Windows Image Parser Using Compositional Exhaustive Testing (MC, PG), pp. 373–392.

VMCAI-2015-UrbanM #abstract interpretation #proving

Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation (CU, AM), pp. 190–208.

ITiCSE-2014-MI #bound #query

A method to prove query lower bounds (JM, SI), pp. 81–86.

TACAS-2014-ChenCFNO #proving #safety

Proving Nontermination via Safety (HYC, BC, CF, KN, PWO), pp. 156–171.

TACAS-2014-Cheval #algorithm #equivalence #named #proving

APTE: An Algorithm for Proving Trace Equivalence (VC), pp. 587–592.

WRLA-2014-LucasM14a #2d #dependence #proving #termination

2D Dependency Pairs for Proving Operational Termination of CTRSs (SL, JM), pp. 195–212.

SAS-2014-UrbanM #abstract domain #proving #termination

A Decision Tree Abstract Domain for Proving Conditional Termination (CU, AM), pp. 302–318.

FLOPS-2014-Bahr #compilation #correctness #graph #proving #using

Proving Correctness of Compilers Using Structured Graphs (PB), pp. 221–237.

DLT-J-2013-GocRRS14 #automation #on the #word

On the number of Abelian Bordered Words (with an Example of Automatic Theorem-Proving) (DG, NR, MR, PS), pp. 1097–1110.

FM-2014-DenmanM #automation #proving

Automated Real Proving in PVS via MetiTarski (WD, CAM), pp. 194–199.

PPDP-2014-AotoS #induction #proving #theorem

Decision Procedures for Proving Inductive Theorems without Induction (TA, SS), pp. 237–248.

PPDP-2014-LucasM #declarative #logic #proving #source code #termination

Proving Operational Termination of Declarative Programs in General Logics (SL, JM), pp. 111–122.

PPDP-2014-MehnerSSV #functional #parametricity #proving #theorem

Parametricity and Proving Free Theorems for Functional-Logic Languages (SM, DS, LS, JV), pp. 19–30.

SPLC-2014-ThumMBHRS #model checking #product line #proving #theorem proving

Potential synergies of theorem proving and model checking for software product lines (TT, JM, FB, MH, AvR, GS), pp. 177–186.

CAV-2014-LarrazNORR #proving #using

Proving Non-termination Using Max-SMT (DL, KN, AO, ERC, AR), pp. 779–796.

IJCAR-2014-BaumgartnerBW #finite #proving #quantifier #theorem proving

Finite Quantification in Hierarchic Theorem Proving (PB, JB, UW), pp. 152–167.

IJCAR-2014-BeyersdorffC #complexity #proving #theorem proving

The Complexity of Theorem Proving in Circumscription and Minimal Entailment (OB, LC), pp. 403–417.

IJCAR-2014-GieslBEFFOPSSST #automation #proving #source code #termination

Proving Termination of Programs Automatically with AProVE (JG, MB, FE, FF, CF, CO, MP, PSK, TS, SS, RT), pp. 184–191.

IJCAR-2014-NigamRL #automation #named #permutation #proving

Quati: An Automated Tool for Proving Permutation Lemmas (VN, GR, LL), pp. 255–261.

IJCAR-2014-StroderGBFFHS #memory management #pointer #proving #safety #source code #termination

Proving Termination and Memory Safety for Programs with Pointer Arithmetic (TS, JG, MB, FF, CF, JH, PSK), pp. 208–223.

RTA-TLCA-2014-AotoTU #confluence #diagrams #proving #term rewriting

Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (TA, YT, KU), pp. 46–60.

ASE-2013-HuangMM #proving #smt #using

Proving MCAPI executions are correct using SMT (YH, EM, JM), pp. 26–36.

TACAS-2013-CookSZ #proving #termination

Ramsey vs. Lexicographic Termination Proving (BC, AS, FZ), pp. 47–61.

CIAA-J-2012-GocHS13 #automation #combinator #word

Automatic Theorem-Proving in Combinatorics on Words (DG, DH, JS), pp. 781–798.

ICALP-v1-2013-LauriaPRT #complexity #graph #proving

The Complexity of Proving That a Graph Is Ramsey (ML, PP, VR, NT), pp. 684–695.

IFM-2013-AndriamiarinaMS #algorithm #distributed #modelling

Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms (MBA, DM, NKS), pp. 268–284.

HILT-2013-Taft #concurrent #named #parallel #proving #safety #source code #thread #tutorial

Tutorial: proving safety of parallel / multi-threaded programs (STT), pp. 1–2.

PPDP-2013-KrienerKB #coq #prolog #proving #semantics

Proofs you can believe in: proving equivalences between Prolog semantics in Coq (JK, AK, SB), pp. 37–48.

SAC-PL-J-2010-PopeeaC13 #analysis #debugging #proving #safety

Dual analysis for proving safety and finding bugs (CP, WNC), pp. 390–411.

CADE-2013-WilliamsK #problem #proving #reduction #satisfiability

Propositional Temporal Proving with Reductions to a SAT Problem (RW, BK), pp. 421–435.

CAV-2013-BrockschmidtCF #proving #termination

Better Termination Proving through Cooperation (MB, BC, CF), pp. 413–429.

CAV-2013-GantyG #proving #termination

Proving Termination Starting from the End (PG, SG), pp. 397–412.

CAV-2013-KovacsV #first-order #proving #theorem proving

First-Order Theorem Proving and Vampire (LK, AV), pp. 1–35.

CSL-2013-Kikuchi #nondeterminism #normalisation #proving #λ-calculus

Proving Strong Normalisation via Non-deterministic Translations into Klop’s Extended λ-Calculus (KK), pp. 395–414.

LICS-2013-HoffmannMS #proving #reasoning

Quantitative Reasoning for Proving Lock-Freedom (JH, MM, ZS), pp. 124–133.

RTA-2013-WinklerZM #automation #proving #sequence #termination

Beyond Peano Arithmetic — Automatically Proving Termination of the Goodstein Sequence (SW, HZ, AM), pp. 335–351.

SAT-2013-Beyersdorff #complexity #logic #proving #theorem proving

The Complexity of Theorem Proving in Autoepistemic Logic (OB), pp. 365–376.

TLCA-2013-Herbelin #proving

Proving with Side Effects (HH), p. 2.

DAC-2012-PurandareAH #correctness #proving #regular expression

Proving correctness of regular expression accelerators (MP, KA, CH), pp. 350–355.

TACAS-2012-HolzerKSTV #contest #proving #reachability #using

Proving Reachability Using FShell — (Competition Contribution) (AH, DK, CS, MT, HV), pp. 538–541.

PLDI-2012-CarbinKMR #approximate #nondeterminism #proving #source code

Proving acceptability properties of relaxed nondeterministic approximate programs (MC, DK, SM, MCR), pp. 169–180.

CIAA-2012-GocHS #automation #combinator #word

Automatic Theorem-Proving in Combinatorics on Words (DG, DH, JS), pp. 180–191.

HILT-2012-Kanig #ada #testing #verification

Leading-edge ada verification technologies: combining testing and verification with GNATTest and GNATProve — the hi-lite project (JK), pp. 5–6.

HILT-2012-Leino12a #proving #using #verification #why

Program proving using intermediate verification languages (IVLs) like boogie and why3 (KRML), pp. 25–26.

LOPSTR-2012-Seki #logic programming #program transformation #proving #source code

Proving Properties of Co-logic Programs with Negation by Program Transformations (HS), pp. 213–227.

CAV-2012-EsparzaGK #probability #proving #source code #termination #using

Proving Termination of Probabilistic Programs Using Patterns (JE, AG, SK), pp. 123–138.

CAV-2012-SchellhornWD #algorithm #how

How to Prove Algorithms Linearisable (GS, HW, JD), pp. 243–259.

IJCAR-2012-EmmesEG #automation #proving

Proving Non-looping Non-termination Automatically (FE, TE, JG), pp. 225–240.

LICS-2012-TraytelPB #category theory #composition #data type #higher-order #logic #proving #theorem proving

Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (DT, AP, JCB), pp. 596–605.

ESOP-2011-BieniusaT #memory management #proving #transaction

Proving Isolation Properties for Software Transactional Memory (AB, PT), pp. 38–56.

TACAS-2011-ChamarthiDMV #proving #theorem proving

The ACL2 Sedan Theorem Proving System (HRC, PCD, PM, DV), pp. 291–295.

SEFM-2011-ErnstSR #analysis #empirical #interactive #proving #theorem proving #verification

Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving (GE, GS, WR), pp. 188–203.

SEFM-2011-JacquelBDD #automation #proving #theorem proving #using #verification

Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving (MJ, KB, DD, CD), pp. 253–268.

ICFP-2011-HinzeJ #category theory #fixpoint #proving

Proving the unique fixed-point principle correct: an adventure with category theory (RH, DWHJ), pp. 359–371.

HCI-ITE-2011-SpiesBLWBH #concept #development #industrial #metric

Measurement of Driver’s Distraction for an Early Prove of Concepts in Automotive Industry at the Example of the Development of a Haptic Touchpad (RS, AB, CL, MW, KB, WH), pp. 125–132.

LOPSTR-2011-Seki #logic programming #proving #source code

Proving Properties of Co-Logic Programs by Unfold/Fold Transformations (HS), pp. 205–220.

SAC-2011-Blech #encryption #logic #proving #security

Proving the security of ElGamal encryption via indistinguishability logic (JOB), pp. 1625–1632.

ESEC-FSE-2011-ChaudhuriGLN #proving #robust #source code

Proving programs robust (SC, SG, RL, SN), pp. 102–112.

CADE-2011-Brown #higher-order #problem #proving #satisfiability #sequence #theorem proving

Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems (CEB), pp. 147–161.

CADE-2011-Cook #liveness #proving #roadmap #termination

Advances in Proving Program Termination and Liveness (BC), p. 4.

CADE-2011-SchneiderS #automation #first-order #ontology #owl #proving #reasoning #theorem proving #using

Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving (MS, GS), pp. 461–475.

RTA-2011-AotoT #confluence #proving #term rewriting

A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems (TA, YT), pp. 91–106.

RTA-2011-NeurauterM #matrix #proving #term rewriting #termination

Revisiting Matrix Interpretations for Proving Termination of Term Rewriting (FN, AM), pp. 251–266.

RTA-2011-ZantemaE #automation #proving #similarity

Proving Equality of Streams Automatically (HZ, JE), pp. 393–408.

TAP-2011-Gaudel #modelling #proving #source code #testing

Checking Models, Proving Programs, and Testing Systems (MCG), pp. 1–13.

VMCAI-2011-CookFKP #biology #proving

Proving Stabilization of Biological Systems (BC, JF, EK, NP), pp. 134–149.

FASE-2010-DarvasM #consistency #proving #using

Proving Consistency and Completeness of Model Classes Using Theory Interpretation (ÁD, PM), pp. 218–232.

WRLA-2010-GutierrezL #dependence #framework #proving #termination

Proving Termination in the Context-Sensitive Dependency Pair Framework (RG, SL), pp. 18–34.

FLOPS-2010-NishidaS #injection #proving #term rewriting

Proving Injectivity of Functions via Program Inversion in Term Rewriting (NN, MS), pp. 288–303.

KEOD-2010-KatsumiG #lifecycle #ontology #proving #theorem proving

Theorem Proving in the Ontology Lifecycle (MK, MG), pp. 37–49.

LOPSTR-2010-HerasPR #correctness #proving #set

Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System (JH, VP, JR), pp. 37–51.

PPDP-2010-Bonacina #on the #proving #theorem proving

On theorem proving for program checking: historical perspective and recent developments (MPB), pp. 1–12.

SAC-2010-PopeeaC #analysis #debugging #proving #safety

Dual analysis for proving safety and finding bugs (CP, WNC), pp. 2137–2143.

SAC-2010-VermolenHL #consistency #modelling #proving #using

Proving consistency of VDM models using HOL (SV, JH, PGL), pp. 2503–2510.

CAV-2010-Vafeiadis #automation #proving

Automatically Proving Linearizability (VV), pp. 450–464.

IJCAR-2010-BaeldeMS #induction #proving #theorem proving

Focused Inductive Theorem Proving (DB, DM, ZS), pp. 278–292.

ISSTA-2010-GodefroidK #float #memory management #program analysis #proving #safety

Proving memory safety of floating-point computations by combining static and dynamic program analysis (PG, JK), pp. 1–12.

LICS-2010-Herbelin #logic #markov #principle

An Intuitionistic Logic that Proves Markov’s Principle (HH), pp. 50–56.

LICS-2010-Moore #proving #theorem proving #verification

Theorem Proving for Verification: The Early Days (JSM), p. 283.

RTA-2010-ZantemaR #data type #infinity #proving

Proving Productivity in Infinite Data Structures (HZ, MR), pp. 401–416.

TAP-2010-GogollaHK #automation #independence #invariant #ocl #proving #testing #visualisation

Proving and Visualizing OCL Invariant Independence by Automatically Generated Test Cases (MG, LH, MK), pp. 38–54.

TAP-2010-Rusu #proving #specification #theorem proving

Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications (VR), pp. 135–150.

WRLA-2008-Rodriguez09

Combining Techniques to Reduce State Space and Prove Strong Properties (DER), pp. 267–280.

FASE-2009-LeinoM #consistency #proving

Proving Consistency of Pure Methods and Model Fields (KRML, RM), pp. 231–245.

PLDI-2009-KunduTL #equivalence #optimisation #proving #using

Proving optimizations correct using parameterized program equivalence (SK, ZT, SL), pp. 327–337.

SAS-2009-Bouissou #algorithm #correctness #implementation #proving

Proving the Correctness of the Implementation of a Control-Command Algorithm (OB), pp. 102–119.

FM-2009-HoenickeLPSW

It’s Doomed; We Can Prove It (JH, KRML, AP, MS, TW), pp. 338–353.

LOPSTR-2009-IborraNV #dependence #proving #termination

Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing (JI, NN, GV), pp. 52–66.

LOPSTR-2009-PilozziSB #approach #constraints #proving

A Transformational Approach for Proving Properties of the CHR Constraint Store (PP, TS, MB), pp. 22–36.

POPL-2009-GotsmanCPV #algorithm #proving

Proving that non-blocking algorithms don’t block (AG, BC, MJP, VV), pp. 16–28.

CADE-2009-BonacinaLM #on the #proving #satisfiability #theorem proving

On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving (MPB, CL, LMdM), pp. 35–50.

CADE-2009-McLaughlinP #performance #proving #theorem proving

Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method (SM, FP), pp. 230–244.

CADE-2009-SutcliffeBBT #automation #development #higher-order #logic #proving #theorem proving

Progress in the Development of Automated Theorem Proving for Higher-Order Logic (GS, CB, CEB, FT), pp. 116–130.

CADE-2009-SwiderskiPGFS #analysis #dependence #induction #proving #termination #theorem proving

Termination Analysis by Dependency Pairs and Inductive Theorem Proving (SS, MP, JG, CF, PSK), pp. 322–338.

CAV-2009-Strichman #equivalence #proving #source code #verification

Regression Verification: Proving the Equivalence of Similar Programs (OS), p. 63.

ICLP-2009-PilozziS #proving #termination

Proving Termination by Invariance Relations (PP, DDS), pp. 499–503.

ICST-2009-PostS #bound #equivalence #functional #implementation #model checking #proving #using

Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking (HP, CS), pp. 31–40.

RTA-2009-AotoYT #automation #confluence #proving #term rewriting

Proving Confluence of Term Rewriting Systems Automatically (TA, JY, YT), pp. 93–102.

RTA-2009-FuhsGPSF #integer #proving #term rewriting #termination

Proving Termination of Integer Term Rewriting (CF, JG, MP, PSK, SF), pp. 32–47.

SAT-2009-BeyersdorffM #question

Does Advice Help to Prove Propositional Tautologies? (OB, SM), pp. 65–72.

TACAS-2008-ClarkeTV #abstraction #concurrent #framework #model checking #proving

Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems (EMC, MT, HV), pp. 33–47.

PEPM-2008-Voigtlander #correctness #proving #theorem

Proving correctness via free theorems: the case of the destroy/build-rule (JV), pp. 13–20.

SAS-2008-ConwayDNB #analysis #fault #pointer #proving

Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors (CLC, DD, KSN, CB), pp. 62–77.

FLOPS-2008-PrinceGM #proving #using

Proving Properties about Lists Using Containers (RP, NG, CM), pp. 97–112.

DLT-2008-HromkovicS #automaton #bound #nondeterminism #on the #proving

On the Hardness of Determining Small NFA’s and of Proving Lower Bounds on Their Sizes (JH, GS), pp. 34–55.

LATA-2008-KorpM #bound #dependence #proving #term rewriting #termination

Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems (MK, AM), pp. 321–332.

GT-VC-2007-Bruggink08 #graph transformation #proving #termination #towards

Towards a Systematic Method for Proving Termination of Graph Transformation Systems (HJSB), pp. 23–38.

ICGT-2008-Pennemann #proving #theorem proving

Resolution-Like Theorem Proving for High-Level Conditions (KHP), pp. 289–304.

KR-2008-Lin #proving

Proving Goal Achievability (FL), pp. 621–628.

POPL-2008-GuptaHMRX #proving

Proving non-termination (AG, TAH, RM, AR, RGX), pp. 147–158.

CAV-2008-CookGLRS #proving #termination

Proving Conditional Termination (BC, SG, TLA, AR, MS), pp. 328–340.

CAV-2008-Harrison #proving #theorem proving #tutorial #verification

Theorem Proving for Verification (Invited Tutorial) (JH), pp. 11–18.

CAV-2008-WienandWSKG #algebra #approach #correctness #proving

An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths (OW, MW, DS, WK, GMG), pp. 473–486.

CSL-2008-Nguyen #proving #using

Proving Infinitude of Prime Numbers Using Binomial Coefficients (PN), pp. 184–198.

IJCAR-2008-KremerMT #protocol #proving

Proving Group Protocols Secure Against Eavesdroppers (SK, AM, RT), pp. 116–131.

IJCAR-2008-Melquiond #bound #proving

Proving Bounds on Real-Valued Functions with Computations (GM), pp. 2–17.

IJCAR-2008-Otten #agile #logic #performance #proving #theorem proving

leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) (JO), pp. 283–291.

RTA-2008-MoserS #polynomial #proving #using

Proving Quadratic Derivational Complexities Using Context Dependent Interpretations (GM, AS), pp. 276–290.

PLDI-2007-CookPR #concurrent #proving #termination #thread

Proving thread termination (BC, AP, AR), pp. 320–330.

IFM-2007-DerrickSW #proving #refinement

Proving Linearizability Via Non-atomic Refinement (JD, GS, HW), pp. 195–214.

SEFM-2007-BabicHRC #proving #termination

Proving Termination by Divergence (DB, AJH, ZR, BC), pp. 93–102.

SEFM-2007-Cook #automation #concurrent #proving #source code

Automatically Proving Concurrent Programs Correct (BC), pp. 269–272.

CEFP-2007-MolEP #functional #lazy evaluation #proving #source code

Proving Properties of Lazy Functional Programs with Sparkle (MdM, MCJDvE, RP), pp. 41–86.

LOPSTR-2007-Codish #proving #termination

Proving Termination with (Boolean) Satisfaction (MC), pp. 1–7.

POPL-2007-CookGPRV #proving #source code

Proving that programs eventually do something good (BC, AG, AP, AR, MYV), pp. 265–276.

CADE-2007-GieslTSS #bound #proving #termination

Proving Termination by Bounded Increase (JG, RT, SS, PSK), pp. 443–459.

CADE-2007-TiwariG #logic #program analysis #proving #theorem proving #using

Logical Interpretation: Static Program Analysis Using Theorem Proving (AT, SG), pp. 147–166.

CAV-2007-Cook #automation #proving #termination

Automatically Proving Program Termination (BC), p. 1.

LICS-2007-NguyenC #complexity #proving #theorem

The Complexity of Proving the Discrete Jordan Curve Theorem (PN, SAC), pp. 245–256.

RTA-2007-KorpM #bound #proving #term rewriting #termination #using

Proving Termination of Rewrite Systems Using Bounds (MK, AM), pp. 273–287.

TAP-2007-Haiyan #algorithm #distributed #proving #testing #type system

Testing and Proving Distributed Algorithms in Constructive Type Theory (QH), pp. 79–94.

TAP-2007-RummerS #calculus #java #logic #proving #source code #using

Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic (PR, MAS), pp. 41–60.

DAC-2006-AwedhS #automation #bound #invariant #model checking

Automatic invariant strengthening to prove properties in bounded model checking (MA, FS), pp. 1073–1076.

DATE-DF-2006-LennardBFIUSWFRB #design #integration #proving #specification

Industrially proving the SPIRIT consortium specifications for design chain integration (CKL, VB, SF, MI, CU, MS, JW, OF, FR, PB), pp. 142–147.

SAS-2006-Bertrane #communication #proving

Proving the Properties of Communicating Imperfectly-Clocked Synchronous Systems (JB), pp. 370–386.

FM-2006-UmenoL #automaton #case study #protocol #proving #safety #theorem proving #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.

SFM-2006-Harrison #float #proving #theorem proving #using #verification

Floating-Point Verification Using Theorem Proving (JH), pp. 211–242.

SFM-2006-Manolios #proving #refinement #theorem proving

Refinement and Theorem Proving (PM), pp. 176–210.

IFL-2006-Kozsik #proving #type system

Proving Program Properties Specified with Subtype Marks (TK), pp. 163–180.

LOPSTR-2006-NguyenS #automation #named #polynomial #proving #termination

Polytool: Proving Termination Automatically Based on Polynomial Interpretations (MTN, DDS), pp. 210–218.

RE-2006-Miller #development #modelling #proving #requirements

Proving the Shalls: Requirements, Proofs, and Model-Based Development (SPM), p. 261.

ICSE-2006-ManoliosV #proving #static analysis #termination #theorem proving

Integrating static analysis and general-purpose theorem proving for termination analysis (PM, DV), pp. 873–876.

PPoPP-2006-VafeiadisHHS #correctness #proving

Proving correctness of highly-concurrent linearisable objects (VV, MH, CARH, MS), pp. 129–136.

ICLP-2006-PettorossiPS #constraints #logic programming #proving #source code

Proving Properties of Constraint Logic Programs by Eliminating Existential Variables (AP, MP, VS), pp. 179–195.

IJCAR-2006-EndrullisWZ #matrix #proving #term rewriting #termination

Matrix Interpretations for Proving Termination of Term Rewriting (JE, JW, HZ), pp. 574–588.

IJCAR-2006-Mahboubi #algorithm #implementation #performance #proving

Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials (AM), pp. 438–452.

ISSTA-2006-YorshBS #abstraction #exclamation #proving #testing #theorem proving

Testing, abstraction, theorem proving: better together! (GY, TB, MS), pp. 145–156.

RTA-2006-BournezG #proving #termination

Proving Positive Almost Sure Termination Under Strategies (OB, FG), pp. 357–371.

RTA-2006-Koprowski06a #automation #named #termination

TPA: Termination Proved Automatically (AK), pp. 257–266.

ASE-2005-GheyiMB #approach #proving #refactoring

A rigorous approach for proving model refactorings (RG, TM, PB), pp. 372–375.

DAC-2005-MonyBPK #proving

Exploiting suspected redundancy without proving it (HM, JB, VP, RK), pp. 463–466.

WRLA-2004-PalominoP05 #maude #model checking #proving

Proving VLRL Action Properties with the Maude Model Checker (MP, IP), pp. 113–133.

SEFM-2005-OlssonW #correctness #imperative #induction #proving #source code

Customised Induction Rules for Proving Correctness of Imperative Programs (OO, AW), pp. 180–189.

SEFM-2005-Trentelman #correctness #proving #using

Proving Correctness of JavaCard DL Taclets using Bali (KT), pp. 160–169.

ICFP-2005-ChenX #programming #proving #theorem proving

Combining programming with theorem proving (CC, HX), pp. 66–77.

AdaEurope-2005-SwardB #equivalence #functional #proving #slicing

Proving Functional Equivalence for Program Slicing in SPARK™ (RES, LCBI), pp. 105–114.

CADE-2005-OgawaHO #incremental #proving

Proving Properties of Incremental Merkle Trees (MO, EH, SO), pp. 424–440.

CAV-2005-CookKS #named #proving #theorem proving #verification

Cogent: Accurate Theorem Proving for Program Verification (BC, DK, NS), pp. 296–300.

RTA-2005-BournezG #proving #termination

Proving Positive Almost-Sure Termination (OB, FG), pp. 323–337.

VMCAI-2005-Cousot #abstraction #parametricity #programming #proving #termination

Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming (PC), pp. 1–24.

FoSSaCS-2004-Lucas #proving #termination

Polynomials for Proving Termination of Context-Sensitive Rewriting (SL), pp. 318–332.

PEPM-2004-DuranLMMU #equation #proving #source code #termination

Proving termination of membership equational programs (FD, SL, JM, CM, XU), pp. 147–158.

IFM-2004-EllisI #automation #integration #program analysis #proving #theorem proving

An Integration of Program Analysis and Automated Theorem Proving (BJE, AI), pp. 67–86.

IFM-2004-Melham #functional #model checking #proving #theorem proving

Integrating Model Checking and Theorem Proving in a Reflective Functional Language (TFM), pp. 36–39.

ICEIS-v1-2004-Augusto #model checking #theorem proving #verification

Model Checking and Theorem Proving-Based Verification of EIS (JCA), p. XXXIII-XXXIV.

PDCL-2004-LindenstraussSS #approach #logic programming #proving #source code #termination

Proving Termination for Logic Programs by the Query-Mapping Pairs Approach (NL, YS, AS), pp. 453–498.

CAV-2004-AwedhS #bound #model checking #proving

Proving More Properties with Bounded Model Checking (MA, FS), pp. 96–108.

CAV-2004-BallCLZ #abstraction #automation #named #proving #refinement #theorem proving

Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement (TB, BC, SKL, LZ), pp. 457–461.

CSL-2004-GanzingerK #equation #proving #reasoning #theorem proving

Integrating Equational Reasoning into Instantiation-Based Theorem Proving (HG, KK), pp. 71–84.

CSL-2004-GiacobazziM #proving

Proving Abstract Non-interference (RG, IM), pp. 280–294.

CSL-2004-Lynch #proving #theorem proving

Unsound Theorem Proving (CL), pp. 473–487.

LICS-2004-Leivant #logic #proving #termination

Proving Termination Assertions in Dynamic Logics (DL), pp. 89–98.

RTA-2004-LimetS #logic programming #proving #source code #term rewriting

Proving Properties of Term Rewrite Systems via Logic Programs (SL, GS), pp. 170–184.

RTA-2004-Lucas #named #proving #termination

mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting (SL), pp. 200–209.

RTA-2004-Zantema #automation #named #termination

TORPA: Termination of Rewriting Proved Automatically (HZ), pp. 95–104.

DAC-2003-GuptaRSBBFPOS #verification

Formal verification — prove it or pitch it (RKG, SR, SKS, BB, DKB, MF, CP, JO, FS), pp. 710–711.

TACAS-2003-Lee #case study #experience #what

What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code (PL0), p. 1.

PLDI-2003-LernerMC #automation #compilation #correctness #optimisation #proving

Automatically proving the correctness of compiler optimizations (SL, TDM, CC), pp. 220–231.

STOC-2003-KabanetsI #bound #polynomial #proving #testing

Derandomizing polynomial identity tests means proving circuit lower bounds (VK, RI), pp. 355–364.

FME-2003-Henderson #correctness #proving #using

Proving the Correctness of Simpson’s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method (NH), pp. 244–263.

FME-2003-MillerTH #proving

Proving the Shalls (SPM, ACT, MPEH), pp. 75–93.

SEFM-2003-DeharbeR #debugging #proving #theorem proving #verification

Light-Weight Theorem Proving for Debugging and Verifying Units of Code (DD, SR), pp. 220–228.

LOPSTR-2003-LehmannL #generative #induction #proving #theorem proving #using

Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce (HL, ML), pp. 1–19.

LOPSTR-2003-SerebrenikS #proving #termination

Proving Termination with Adornments (AS, DDS), pp. 108–109.

CADE-2003-AvenhausKSW #exclamation #how #induction #theorem

How to Prove Inductive Theorems? QUODLIBET! (JA, UK, TSS, CPW), pp. 328–333.

CADE-2003-MehtaN #higher-order #logic #pointer #proving #source code

Proving Pointer Programs in Higher-Order Logic (FM, TN), pp. 121–135.

CAV-2003-FlanaganJOS #lazy evaluation #proving #theorem proving #using

Theorem Proving Using Lazy Proof Explication (CF, RJ, XO, JBS), pp. 355–367.

FATES-2003-HahnleW #proving #testing #theorem proving #using

Using a Software Testing Technique to Improve Theorem Proving (RH, AW), pp. 30–41.

LICS-2003-GanzingerK #proving #theorem proving

New Directions in Instantiation-Based Theorem Proving (HG, KK), pp. 55–64.

FoSSaCS-2002-BoerGM #concurrent #constraints #correctness #proving #source code

Proving Correctness of Timed Concurrent Constraint Programs (FSdB, MG, MCM), pp. 37–51.

FoSSaCS-2002-JancarKMS #automaton #bound #proving

Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds (PJ, AK, FM, ZS), pp. 172–186.

SAS-2002-VeldhuizenL #compilation #optimisation #proving

Guaranteed Optimization: Proving Nullspace Properties of Compilers (TLV, AL), pp. 263–277.

IFL-2002-DowseSB #haskell #proving

Proving Make Correct: I/O Proofs in Haskell and Clean (MD, GS, AB), pp. 68–83.

ICEIS-2002-HillbrandK #approach #metamodelling #network #using

Using Artificial Neural Networks to Prove Hypothetic Cause-And-Effect Relations: A Metamodel-Based Approach to Support Strategic Decisions (CH, DK), pp. 367–373.

POPL-2002-LaceyJWF #compilation #correctness #logic #optimisation #proving

Proving correctness of compiler optimizations by temporal logic (DL, NDJ, EVW, CCF), pp. 283–294.

CADE-2002-Brown #higher-order #proving #set #theorem proving

Solving for Set Variables in Higher-Order Theorem Proving (CEB), pp. 408–422.

CADE-2002-MouraRS #bound #infinity #lazy evaluation #model checking #proving #theorem proving

Lazy Theorem Proving for Bounded Model Checking over Infinite Domains (LMdM, HR, MS), pp. 438–455.

CAV-2002-BlomP #confluence #proving #reduction

State Space Reduction by Proving Confluence (SB, JvdP), pp. 596–609.

CAV-2002-ColonS #proving #termination

Practical Methods for Proving Program Termination (MC, HS), pp. 442–454.

CAV-2002-Jacobi #model checking #pipes and filters #verification

Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving (CJ0), pp. 309–323.

ICLP-2002-Craciunescu #equivalence #proving #source code

Proving the Equivalence of CLP Programs (SC), pp. 287–301.

ISSTA-2002-ChenTZ #evaluation #named #symbolic computation #testing

Semi-proving: an integrated method based on global symbolic evaluation and metamorphic testing (TYC, THT, ZZ), pp. 191–195.

TestCom-2002-CastanetR #analysis #proving #reachability #testing #theorem proving

Generate Certified Test Cases by Combining Theorem Proving and Reachability Analysis (RC, DR), pp. 249–266.

VMCAI-2002-GenaimCGL #termination

Combining Norms to Prove Termination (SG, MC, JPG, VL), pp. 126–138.

FASE-2001-InverardiU #component #concurrent #programming #proving

Proving Deadlock Freedom in Component-Based Programming (PI, SU), pp. 60–75.

FLOPS-J2-1998-Sakurai01 #category theory #proving

Categorical Model Construction for Proving Syntactic Properties (TS), pp. 213–244.

FLOPS-2001-PolakovY #exception #framework #logic #order #proving

Proving Syntactic Properties of Exceptions in an Ordered Logical Framework (JP, KY), pp. 61–77.

IFL-2001-ButterfieldS #comparison #correctness #paradigm #proving #source code

Proving Correctness of Programs with IO — A Paradigm Comparison (AB, GS), pp. 72–87.

IFL-2001-EncinaP #correctness #proving

Proving the Correctness of the STG Machine (AdlE, RP), pp. 88–104.

IFL-2001-MolEP #functional #proving #theorem proving

Theorem Proving for Functional Programmers (MdM, MCJDvE, MJP), pp. 55–71.

SAIG-2001-Johann

Short Cut Fusion: Proved and Improved (PJ), pp. 47–71.

ICLP-2001-DrabentM #approach #correctness #declarative #proving #source code

Proving Correctness and Completeness of Normal Programs — A Declarative Approach (WD, MM), pp. 284–299.

IJCAR-2001-NieuwenhuisHRV #evaluation #on the #proving #theorem proving

On the Evaluation of Indexing Techniques for Theorem Proving (RN, TH, AR, AV), pp. 257–271.

IJCAR-2001-SchmittLKN #interactive #proving #theorem proving

JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants (SS, LL, CK, AN), pp. 421–426.

RTA-2001-Barendregt #proving

Computing and Proving (HB), p. 1.

SAT-2001-Goldberg #proving #satisfiability

Proving unsatisfiability of CNFs locally (EG), pp. 96–114.

SAT-2001-McllraithA #proving #theorem proving

Theorem Proving with Structured Theories (Preliminary Report)* (SM, EA), pp. 311–328.

UML-2000-Padawitz #constraints #diagrams #how #proving #state machine #theorem proving #uml

Swinging UML: How to Make Class Diagrams and State Machines Amenable to Constraint Solving and Proving (PP), pp. 162–177.

CADE-2000-AndrewsB #education #higher-order #logic #named #proving #theorem proving #tutorial #using

Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic (PBA, CEB), pp. 511–512.

CADE-2000-AndrewsBB #proving #theorem proving #type system

System Description: TPS: A Theorem Proving System for Type Theory (PBA, MB, CEB), pp. 164–169.

CADE-2000-Harrison #proving #theorem proving #using #verification

High-Level Verification Using Theorem Proving and Formalized Mathematics (JH), pp. 1–6.

CADE-2000-Seger #float #model checking #proving #theorem proving

Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice (CJHS), p. 235.

CL-2000-HahnleHS #constraints #finite #generative #proving #theorem proving

Moder Generation Theorem Proving with Finite Interval Constraints (RH, RH, YS), pp. 285–299.

CL-2000-Lopez-FraguasH #functional #logic programming #proving #source code

Proving Failure in Functional Logic Programs (FJLF, JSH), pp. 179–193.

LICS-2000-McMillan #model checking #proving #theorem

Some Strategies for Proving Theorems with a Model Checker (KLM), pp. 305–306.

LICS-2000-Voronkov #calculus #how #logic #proving

How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi (AV), pp. 401–412.

FASE-1999-LuthTKK #development #proving #theorem proving #tool support

TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving (CL, HT, K, BKB), pp. 239–243.

TACAS-1999-Pusch #bytecode #higher-order #java #proving #specification #verification

Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL (CP), pp. 89–103.

TACAS-1999-RusuS #abstraction #on the #proving #safety #static analysis #theorem proving

On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction (VR, ES), pp. 178–192.

FM-v2-1999-Nadjm-TehraniA #design #modelling #proving #theorem proving

Combining Theorem Proving and Continuous Models in Synchronous Design (SNT, OÅ), pp. 1384–1399.

CADE-1999-Artemov #on the #proving #theorem proving #verification

On Explicit Reflection in Theorem Proving and Formal Verification (SNA), pp. 267–281.

CADE-1999-FrankeK #automation #communication #distributed #proving #theorem proving

System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving (AF, MK), pp. 217–221.

CADE-1999-Hickey #distributed #fault tolerance #proving #theorem proving

Fault-Tolerant Distributed Theorem Proving (JH), pp. 227–231.

CAV-1999-ManoliosNS #bisimulation #model checking #proving #theorem proving

Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation (PM, KSN, RS), pp. 369–379.

CAV-1999-SaidiS

Abstract and Model Check While You Prove (HS, NS), pp. 443–454.

CSL-1999-Howe #interactive #proving #theorem proving #type system #using

Interactive Theorem Proving Using Type Theory (DJH), p. 578.

ICLP-1999-Smaus #logic programming #proving #source code #termination

Proving Termination of Input-Consuming Logic Programs (JGS), pp. 335–349.

LICS-1999-Paulson #protocol #proving #security

Proving Security Protocols Correct (LCP), pp. 370–381.

DAC-1998-AagaardJS #evaluation #industrial #proving #theorem proving

Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment (MA, RBJ, CJHS), pp. 538–541.

WRLA-1998-CarabettaDG #logic #semantics

CCS semantics via proved transition systems and rewriting logic (GC, PD, FG), pp. 369–387.

FLOPS-1998-Sakurai #proving

Categorial Model Construction for Proving Syntactic Properties (TS), pp. 187–206.

ICALP-1998-Lugiez #automaton #induction #proving #theorem proving

A Good Class of Tree Automata and Application to Inductive Theorem Proving (DL), pp. 409–420.

WIA-1998-LHerPM #automaton #proving #source code #using

Proving Sequential Function Chart Programs Using Automata (DL, PLP, LM), pp. 149–163.

FM-1998-GoerigkH #compilation #correctness #how #implementation

Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct (WG, UH), pp. 122–136.

CADE-1998-FeveW #algebra #geometry #proving #theorem #using

Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules (SF, DW), pp. 17–31.

CADE-1998-FleuriotP #analysis #geometry #proving #standard #theorem proving

A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia (JDF, LCP), pp. 3–16.

CADE-1998-SchurmannP #automation #logic #proving #theorem proving

Automated Theorem Proving in a Simple Meta-Logic for LF (CS, FP), pp. 286–300.

CAV-1998-Camilleri #design #multi #proving #theorem proving

A Role for Theorem Proving in Multi-Processor Design (AJC), pp. 45–48.

SAS-1997-PanitzS #automation #functional #higher-order #named #proving #source code #strict #termination

TEA: Automatically Proving Termination of Programs in a Non-strict Higher-Order Functional Language (SEP, MSS), pp. 345–360.

FME-1997-AgerholmF #automation #proving #theorem proving #towards

Towards an Integrated CASE and Theorem Proving Tool for VDM-SL (SA, JF), pp. 278–297.

FME-1997-Stringer-CalvertSW #case study #refinement #using

Using PVS to Prove a Z Refinement: A Case Study (DWJSC, SS, IW), pp. 573–588.

CADE-1997-DahnGHW #automation #integration #interactive #proving #theorem proving

Integration of Automated and Interactive Theorem Proving in ILP (BID, JG, TH, AW), pp. 57–60.

CADE-1997-FeltyH #hybrid #interactive #proving #theorem proving #using

Hybrid Interactive Theorem Proving Using Nuprl and HOL (APF, DJH), pp. 351–365.

CADE-1997-HasegawaIOK #bottom-up #proving #set #theorem proving #top-down

Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving (RH, KI, YO, MK), pp. 176–190.

CADE-1997-ReifSS #correctness #proving

Proving System Correctness with KIV 3.0 (WR, GS, KS), pp. 69–72.

RTA-1997-ArtsG #automation #normalisation #proving

Proving Innermost Normalisation Automatically (TA, JG), pp. 157–171.

RTA-1997-KapurS #order #proving #term rewriting #termination

A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems (DK, GS), pp. 142–156.

RTA-1997-KuhlerW #data type #equation #induction #proving #specification #theorem proving

Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving (UK, CPW), pp. 38–52.

TLCA-1997-Ruess #calculus #proving #theorem proving

Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving (HR), pp. 319–335.

TACAS-1996-Saidi #automation #concurrent #proving

A Tool for Proving Invariance Properties of Concurrent Systems Automatically (HS), pp. 412–416.

SAS-1996-BoerGP #constraints #correctness #logic programming #proving #scheduling #source code

Proving Correctness of Constraint Logic Programs with Dynamic Scheduling (FSdB, MG, CP), pp. 83–97.

ICALP-1996-Ganzinger #proving #theorem proving

Saturation-Based Theorem Proving (Abstract) (HG), pp. 1–3.

FME-1996-HavelundS #model checking #protocol #proving #theorem proving #verification

Experiments in Theorem Proving and Model Checking for Protocol Verification (KH, NS), pp. 662–681.

POPL-1996-HughesPS #correctness #proving #using

Proving the Correctness of Reactive Systems Using Sized Types (JH, LP, AS), pp. 410–423.

CADE-1996-DenzingerS #learning #proving #theorem proving

Learning Domain Knowledge to Improve Theorem Proving (JD, SS), pp. 62–76.

CADE-1996-Ganzinger #proving #theorem proving

Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract) (HG), p. 1.

CADE-1996-GanzingerW #monad #proving #theorem proving

Theorem Proving in Cancellative Abelian Monoids (Extended Abstract) (HG, UW), pp. 388–402.

CADE-1996-KolbeW #proving #reuse #termination #theorem proving

Termination of Theorem Proving by Reuse (TK, CW), pp. 106–120.

CADE-1996-Luz-Filho #logic #proving #specification #theorem proving

Grammar Specification in Categorial Logics and Theorem Proving (SFLF), pp. 703–717.

CADE-1996-Martin #proving #theorem proving

Theorem Proving with Group Presentations: Examples and Questions (UM), pp. 358–372.

CADE-1996-MelisW #proving #theorem proving

Internal Analogy in Theorem Proving (EM, JW), pp. 92–105.

CAV-1996-ClarkeGZ #algorithm #proving #theorem proving #using #verification

Verifying the SRT Division Algorithm Using Theorem Proving Techniques (EMC, SMG, XZ), pp. 111–122.

CAV-1996-GrafS #invariant #proving #theorem proving #using #verification

Verifying Invariants Using theorem Proving (SG, HS), pp. 196–207.

JICSLP-1996-AravindanBDFNNSS #logic programming #on the #paradigm #proving #theorem proving

On Merging Theorem Proving and Logic Programming Paradigms (Poster Abstract) (CA, PB, JD, UF, GN, IN, DS, FS), p. 546.

RTA-1996-BoudetCM #proving #theorem proving #unification

AC-Complete Unification and its Application to Theorem Proving (AB, EC, CM), pp. 18–32.

RTA-1996-Gramlich #on the #proving #termination

On Proving Termination by Innermost Termination (BG), pp. 93–107.

RTA-1996-HillenbrandBF #on the #performance #proving #theorem proving

On Gaining Efficiency in Completion-Based Theorem Proving (TH, AB, RF), pp. 432–435.

RTA-1996-Stuber #integer #proving #theorem proving

Superposition Theorem Proving for Albelian Groups Represented as Integer Modules (JS), pp. 33–47.

PEPM-1995-Metayer #data type #proving #recursion #source code

Proving Properties of Programs Defined over Recursive Data Structures (DLM), pp. 88–99.

LOPSTR-1995-Renault #logic programming #proving #source code #towards

Towards a Complete Proof Procedure to Prove Properties of Normal Logic Programs under the Completion (SR), pp. 204–218.

SAC-1995-Bsaies #logic programming #proving

Discovering and proving logic program properties (KB), pp. 369–373.

CAV-1995-DingelF #abstraction #infinity #model checking #proving #reasoning #theorem proving #using

Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving (JD, TF), pp. 54–69.

ICLP-1995-Hirata #correctness #haskell #proving #π-calculus

Proving Correctness of Translation from Moded Flat GHC to π-Calculus (KH), p. 818.

ILPS-1995-MarchioriT #logic programming #proving #source code #termination

Proving Termination of Logic Programs with Delay Declarations (EM, FT), pp. 447–461.

RTA-1995-Kuper #proving #reduction

Proving the Genericity Lemma by Leftmost Reduction is Simple (JK), pp. 271–278.

RTA-1995-Stickel #proving #term rewriting #theorem proving

Term Rewriting in Contemporary Resolution Theorem Proving (Abstract) (MES), p. 101.

ALP-1994-BidoitH #behaviour #first-order #logic #proving #standard #theorem

Proving Behavioural Theorems with Standard First-Order Logic (MB, RH), pp. 41–58.

ALP-1994-CodishM #algebra #approximate #proving

Proving Implications by Algebraic Approximation (MC, GM), pp. 6–22.

POPL-1994-BoerGMP #concurrent #constraints #proving #source code

Proving Concurrent Constraint Programs Correct (FSdB, MG, EM, CP), pp. 98–108.

CADE-1994-BeckertP #agile #named #proving #theorem proving

leanTAP: Lean Tableau-Based Theorem Proving (Extended Abstract) (BB, JP), pp. 793–797.

CADE-1994-BonacinaM #distributed #proving #theorem proving

Distributed Theorem Proving by Peers (MPB, WM), pp. 841–845.

CADE-1994-ChuP #first-order #proving #semantics #theorem proving #using

Semantically Guided First-Order Theorem Proving using Hyper-Linking (HC, DAP), pp. 192–206.

CADE-1994-ClarkeZ #problem #proving #symbolic computation #theorem proving

Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan (EMC, XZ), pp. 758–763.

CADE-1994-FeltyH #proving #theorem proving

Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables (APF, DJH), pp. 605–619.

CADE-1994-Goubault #proving

Proving with BDDs and Control of Information (JG), pp. 499–513.

CADE-1994-McPheeCG #geometry #proving #theorem #using

Mechanically Proving Geometry Theorems Using a Combination of Wu’s Method and Collins’ Method (NFM, SCC, XSG), pp. 401–415.

CADE-1994-Plaisted #performance #proving #theorem proving

The Search Efficiency of Theorem Proving Strategies (DAP), pp. 57–71.

CADE-1994-WaalG #logic programming #program analysis #program transformation #proving #theorem proving

The Applicability of Logic Program Analysis and Transformation to Theorem Proving (DAdW, JPG), pp. 207–221.

CADE-1994-Wang #algebra #geometry #proving

Algebraic Factoring and Geometry Proving (DW), pp. 386–400.

ICLP-1994-BreuerSK #design #hardware #proving

Proving Hardware Designs (PTB, LS, CDK), p. 745.

DAC-1993-JoyceS #evaluation #interactive #symbolic computation

Linking BDD-Based Symbolic Evaluation to Interactive Theorem-Proving (JJJ, CJHS), pp. 469–474.

PLILP-1993-BurnM #analysis #compilation #correctness #optimisation #proving #strict

Proving the Correctness of Compiler Optimizations Based on Strictness Analysis (GLB, DLM), pp. 346–364.

CAV-1993-Hungar #model checking #parallel #process #proving #theorem proving #verification

Combining Model Checking and Theorem Proving to Verify Parallel Processes (HH), pp. 154–165.

ICLP-1993-McCarty #higher-order #induction #logic #prolog #proving #source code

Proving Inductive Properties of Prolog Programs in Second-Order Intuitionistic Logic (LTM), pp. 44–63.

ICLP-1993-RaoKS #haskell #proving #source code #termination

Proving Termination of GHC Programs (MRKKR, DK, RKS), pp. 720–736.

ILPS-1993-KirschenbaumS #prolog #proving #source code

Enhancement Structures for Proving Prolog Programs Correct (MK, LS), p. 631.

RTA-1993-AvenhausD #equation #proving #theorem proving

Distributing Equational Theorem Proving (JA, JD), pp. 62–76.

RTA-1993-Bachmair #proving #theorem proving

Rewrite Techniques in Theorem Proving (Abstract) (LB), p. 1.

RTA-1993-Gallier #proving

Proving Properties of Typed λ Terms: Realizability, Covers, and Sheaves (Abstract) (JHG), p. 136.

ESOP-1992-BernsteinRS #proving #safety

Proving Safety of Speculative Load Instructions at Compile Time (DB, MR, SS), pp. 56–72.

ESOP-1992-Gnaedig #proving #specification #theorem proving

ELIOS-OBJ Theorem Proving in a Specification Language (IG), pp. 182–199.

ICALP-1992-DeganoP

Proved Trees (PD, CP), pp. 629–640.

LFP-1992-ChirimarGR #invariant #linear #logic #memory management #proving

Proving Memory Management Invariants for a Language Based on Linear Logic (JC, CAG, JGR), pp. 139–150.

LFP-1992-WandO #correctness #proving

Proving the Correctness of Storage Representations (MW, DO), pp. 151–160.

ALP-1992-BachmairGW #first-order #proving #theorem proving

Theorem Proving for Hierarchic First-Order Theories (LB, HG, UW), pp. 420–434.

CADE-1992-AlexanderP #proving #similarity #theorem

Proving Equality Theorems with Hyper-Linking (GDA, DAP), pp. 706–710.

CADE-1992-Chen #empirical #knowledge-based #proving #theorem proving

Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic (WZC), pp. 552–566.

CADE-1992-ChouG #geometry #proving

Proving Geometry Statements of Constructive Type (SCC, XSG), pp. 20–34.

CADE-1992-Dafa #automation #deduction #proving #theorem proving

A Natural Deduction Automated Theorem Proving System (LD), pp. 668–672.

CADE-1992-NieuwenhuisR #proving #theorem proving

Theorem Proving with Ordering Constrained Clauses (RN, AR), pp. 477–491.

CADE-1992-Voronkov #logic #proving #standard #theorem proving

Theorem Proving in Non-Standard Logics Based on the Inverse Method (AV), pp. 648–662.

CADE-1992-ZhangH #induction #proving #set #theorem

Proving the Chinese Remainder Theorem by the Cover Set Induction (HZ, XH), pp. 431–445.

CSL-1992-Creignou #linear #problem #proving #satisfiability

The Class of Problems that are Linear Equivalent to Satisfiability or a Uniform Method for Proving NP-Completeness (NC), pp. 115–133.

JICSLP-1992-BronsardLR #framework #logic programming #proving #source code #termination

A Framework of Directionality for Proving Termination of Logic Programs (FB, TKL, USR), pp. 321–335.

VDME-1991-1-Clement #development

Combining Transformation and Posit-and Prove in a VDM Development (TC), pp. 63–80.

KR-1991-HalpernV #model checking #proving #theorem proving

Model Checking vs. Theorem Proving: A Manifesto (JYH, MYV), pp. 325–334.

CAV-1991-Mutz #behaviour #correctness #proving #term rewriting #using

Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior (MM), pp. 277–287.

CSL-1991-RaoKS #logic programming #proving #source code #termination

A Transformational Methodology for Proving Termination of Logic Programs (MRKKR, DK, RKS), pp. 213–226.

CSL-1991-Weiermann #proving #term rewriting #termination

Proving Termination for Term Rewriting Systems (AW), pp. 419–428.

ICLP-1991-ColussiM #axiom #correctness #logic programming #proving #semantics #source code #using

Proving Correctness of Logic Programs Using Axiomatic Semantics (LC, EM), pp. 629–642.

ICLP-1991-Hagiya #higher-order #proving #theorem proving #unification

Higher-Order Unification as a Theorem Proving Procedure (MH), pp. 270–284.

ICLP-1991-Lever #proving

Proving Program Properties by Means of SLS-Resolution (JML), pp. 614–628.

LICS-1991-HuttelS #process #proving #similarity #word

Actions Speak Louder than Words: Proving Bisimilarity for Context-Free Processes (HH, CS), pp. 376–386.

LICS-1991-PeledKP #logic #proving #specification

Specifying and Proving Serializability in Temporal Logic (DP, SK, AP), pp. 232–244.

RTA-1991-Avenhaus #equation #induction #proving #theorem

Proving Equational and Inductive Theorems by Completion and Embedding Techniques (JA), pp. 361–373.

RTA-1991-BonacinaH #on the #proving #theorem proving

On Fairness of Completion-Based Theorem Proving Strategies (MPB, JH), pp. 348–360.

RTA-1991-Hermann #on the #proving

On Proving Properties of Completion Strategies (MH), pp. 398–410.

ICALP-1990-PeledP #liveness #partial order #proving

Proving Partial Order Liveness Properties (DP, AP), pp. 553–571.

ALP-1990-Farres-Casals #correctness #proving #specification

Proving Correctness wrt Specifications with Hidden Parts (JFC), pp. 25–39.

ALP-1990-Goguen #proving

Proving and Rewriting (JAG), pp. 1–24.

CADE-1990-AndrewsINP #proving #theorem proving

The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 641–642.

CADE-1990-ChouG #algorithm #composition #geometry #proving #theorem proving

Ritt-Wu’s Decomposition Algorithm and Geometry Theorem Proving (SCC, XSG), pp. 207–220.

CADE-1990-CostaHLS #automation #implementation #logic #proving #theorem proving

Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation (NCAdC, LJH, JJL, VSS), pp. 72–86.

CADE-1990-Hagiya #higher-order #programming #proving #unification #using

Programming by Example and Proving by Example Using Higher-order Unification (MH), pp. 588–602.

CADE-1990-HeiselRS #proving #theorem proving #verification

Tactical Theorem Proving in Program Verification (MH, WR, WS), pp. 117–131.

CADE-1990-HsiangJ #proving #theorem proving #tutorial

Tutorial on Rewrite-Based Theorem Proving (JH, JPJ), p. 684.

CADE-1990-LuskM #automation #proving #theorem proving #tutorial

Tutorial on High-Performance Automated Theorem Proving (ELL, WM), p. 681.

CADE-1990-Tuominen #framework #logic #proving #theorem proving

Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic (HT), pp. 514–527.

SEKE-1989-Cooke #design #proving

Proving Properties of Software Design Methods (DEC), pp. 9–12.

DAC-1988-MadreB #behaviour #comparison #correctness #proving #using

Proving Circuit Correctness Using Formal Comparison Between Expected and Extracted Behaviour (JCM, JPB), pp. 205–210.

ICALP-1988-Culik #decidability #equivalence #problem #proving

New Techniques for Proving the Decidability of Equivalence Problems (KCI), pp. 162–175.

VDME-1988-JonesM #design #empirical #named #proving #theorem proving #user interface

MUFFIN: A User Interface Design Experiment for a Theorem Proving Assistant (CBJ, RCM), pp. 337–375.

ALP-1988-HofbauerK #induction #proving #term rewriting #theorem

Proving Inductive Theorems Based on Term Rewriting Systems (DH, RDK), pp. 180–190.

CADE-1988-AndrewsINP #proving #theorem proving

The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 760–761.

CADE-1988-Hines #knowledge-based #proving #theorem proving

Hyper-Chaining and Knowledge-Based Theorem Proving (LMH), pp. 469–486.

CADE-1988-McRobbieMT #automation #knowledge-based #logic #performance #proving #standard #theorem proving #towards

Towards Efficient “Knowledge-Based” Automated Theorem Proving for Non-Standard Logics (MAM, RKM, PBT), pp. 197–217.

CADE-1988-WosM #automation #challenge #combinator #logic #problem #similarity #source code

Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs (LW, WM), pp. 714–729.

CADE-1988-ZhangK #first-order #proving #theorem proving #using

First-Order Theorem Proving Using Conditional Rewrite Rules (HZ, DK), pp. 1–20.

CSL-1988-DaneluttoM #approach #concurrent #finite #logic

A temporal Logic Approach to Specify and to Prove Properties of Finite State Concurrent Systems (MD, AM), pp. 63–79.

LICS-1988-Baudinet #approach #prolog #proving #semantics #source code #termination

Proving Termination Properties of Prolog Programs: A Semantic Approach (MB), pp. 336–347.

LICS-1988-Tiomkin #proving

Proving unprovability (MLT), pp. 22–26.

CSL-1987-BryM #database #deduction #finite #proving #satisfiability

Proving Finite Satisfiability of Deductive Databases (FB, RM), pp. 44–55.

CSL-1987-Schoning #complexity

Complexity Cores and Hard-To-Prove Formulas (US), pp. 273–280.

LICS-1987-AlpernS #proving

Proving Boolean Combinations of Deterministic Properties (BA, FBS), pp. 131–137.

LICS-1987-BachmairD #first-order #proving #theorem proving

Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.

LICS-1987-GallierRS #equation #proving #theorem proving #using

Theorem Proving Using Rigid E-Unification Equational Matings (JHG, SR, WS), pp. 338–346.

ESOP-1986-Stark #concept #proving #specification

Proving Entailment Between Conceptual State Specifications (EWS), pp. 197–209.

CADE-1986-AbadiM #proving #theorem proving

Modal Theorem Proving (MA, ZM), pp. 172–189.

CADE-1986-AndrewsPIK #proving #theorem proving

The TPS Theorem Proving System (PBA, FP, SI, CPK), pp. 663–664.

CADE-1986-BeierleOV #automation #proving #theorem proving

Automatic Theorem Proving in the ISDV System (CB, WGO, AV), pp. 670–671.

CADE-1986-BiundoHHW #induction #proving #theorem proving

The Karlsruhe Induction Theorem Proving System (SB, BH, DH, CW), pp. 672–674.

CADE-1986-ButlerLMO #automation #proving #theorem proving

Paths to High-Performance Automated Theorem Proving (RB, ELL, WM, RAO), pp. 588–597.

CADE-1986-CherifaL #implementation #polynomial #term rewriting #termination

An Actual Implementation of a Procedure That Mechanically Proves Termination of Rewriting Systems Based on Inequalities Between Polynomial Interpretations (ABC, PL), pp. 42–51.

CADE-1986-GnaedigL #commutative #proving #term rewriting #termination

Proving Termination of Associative Commutative Rewriting Systems by Rewriting (IG, PL), pp. 52–61.

CADE-1986-HsiangR #proving #theorem proving

A New Method for Establishing Refutational Completeness in Theorem Proving (JH, MR), pp. 141–152.

CADE-1986-Huet86a #proving #theorem proving

Theorem Proving Systems of the Formel Project (GPH), pp. 687–688.

CADE-1986-LoganantharajM #graph #parallel #proving #theorem proving

Parallel Theorem Proving with Connection Graphs (RL, RAM), pp. 337–352.

CADE-1986-ThistlewaiteMM #automation #proving #theorem proving

The KRIPKE Automated Theorem Proving System (PBT, MAM, RKM), pp. 705–706.

CADE-1986-Toyama #equivalence #how #induction #term rewriting

How to Prove Equivalence of Term Rewriting Systems without Induction (YT), pp. 118–127.

LICS-1986-ChouK #geometry #on the #proving #theorem proving

On Mechanical Theorem Proving in Minkowskian Plane Geometry (SCC, HPK), pp. 187–192.

LICS-1986-Mason #equivalence #first-order #lisp #proving #source code

Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via Transformation (IAM), pp. 105–117.

RTA-1985-ChoppyJ #named #petri net #proving #term rewriting

PETRIREVE: Proving Petri Net Properties with Rewriting Systems (CC, CJ), pp. 271–286.

RTA-1985-DetlefsF #automation #proving #set #termination

A Procedure for Automatically Proving the Termination of a Set of Rewrite Rules (DD, RF), pp. 255–270.

RTA-1985-Hsiang #proving #term rewriting #theorem proving

Two Results in Term Rewriting Theorem Proving (JH), pp. 301–324.

CADE-1984-Plaisted #analysis #dependence #graph #proving #theorem proving #using

Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving (DAP), pp. 356–374.

CADE-1984-Stickel #case study #commutative #proving #theorem proving

A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity (MES), pp. 248–258.

ICALP-1983-HsiangD #proving #theorem proving

Rewrite Methods for Clausal and Non-Clausal Theorem Proving (JH, ND), pp. 331–346.

ICALP-1983-MannaP #precedence #proving

Proving Precedence Properties: The Temporal Way (ZM, AP), pp. 491–512.

POPL-1983-NagleJ #automation #embedded #proving #realtime #verification

Practical Program Verification: Automatic Program Proving for Real-Time Embedded Software (JN, SJ), pp. 48–58.

STOC-1982-PachlKR #algorithm #bound #distributed #proving

A Technique for Proving Lower Bounds for Distributed Maximum-Finding Algorithms (JKP, EK, DR), pp. 378–382.

CADE-1982-Wos #automation

Solving Open Questions with an Automated Theorem-Proving Program (LW), pp. 1–31.

ILPC-1982-BarbutiDL82 #logic programming #proving #source code #towards

Toward an Inductionless Technique for Proving Properties of Logic Programs (RB, PD, GL), pp. 175–181.

DAC-1981-McFarland #automation #correctness #design #on the #optimisation #proving

On proving the correctness of optimizing transformations in a digital design automation system (MCM), pp. 90–97.

ICALP-1981-Snir #bound #proving

Proving Lower Bounds for Linar Decision Trees (MS), pp. 305–315.

ICSE-1981-RamamrithamK #process #proving #specification

Specifying and Proving Properties of Sentinel Processes (KR, RMK), pp. 374–386.

SOSP-1981-BernsteinH #logic #proving #realtime #source code

Proving Real-Time Properties of Programs with Temporal Logic (AJB, PKHJ), pp. 1–11.

ICALP-1980-Turchin #optimisation #proving #theorem proving

The Use of Metasystem Transition in Theorem Proving and Program Optimization (VFT), pp. 645–657.

POPL-1980-Musser #data type #induction #on the #proving

On Proving Inductive Properties of Abstract Data Types (DRM), pp. 154–162.

SDCG-1980-ThatcherWW #compilation #proving

More on advice on structuring compilers and proving them correct (JWT, EGW, JBW), pp. 165–188.

CADE-1980-Guguen #algebra #how #induction

How to Prove Algebraic Inductive Hypotheses Without Induction (JAG), pp. 356–373.

CADE-1980-Kott #proving #recursion #source code

A System for Proving Equivalences of Recursive Programs (LK), pp. 63–69.

CADE-1980-Nederpelt #approach #proving #theorem proving #λ-calculus

An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus (RN), pp. 182–194.

CADE-1980-OverbeekL #architecture #data type #implementation #source code

Data Structures and Control Architectures for Implementation of Theorem-Proving Programs (RAO, ELL), pp. 232–249.

CADE-1980-Plaisted #abstraction #proving #theorem proving

Abstraction Mappings in Mechanical Theorem Proving (DAP), pp. 264–280.

VLDB-1979-GardarinM #consistency #database #proving #transaction

Proving Consistency of Database Transactions (GG, MAM), pp. 291–298.

ICALP-1979-DershowitzM #multi #order #proving #termination

Proving termination with Multiset Orderings (ND, ZM), pp. 188–202.

ICALP-1979-DuncanY #algorithm #correctness #proving

Studies in Abstract/Concrete Mappings in Proving Algorithm Correctness (AGD, LY), pp. 218–229.

ICALP-1979-ThatcherWW #compilation #proving

More on Advice on Structuring Compilers and Proving Them Correct (JWT, EGW, JBW), pp. 596–615.

POPL-1979-GoodC #proving #source code

Principles of Proving Programs Correct in Gypsy (DIG, RMC, JKW), pp. 42–52.

STOC-1977-HarelPS #axiom #deduction #proving #recursion #source code

A Complete Axiomatic System for Proving Deductions about Recursive Programs (DH, AP, JS), pp. 249–260.

SOSP-1977-FeiertagLR #design #multi #proving #security

Proving Multilevel Security of a System Design (RJF, KNL, LR), pp. 57–65.

ICALP-1976-Brand #proving #source code

Proving Programs Incorrect (DB), pp. 201–227.

ICALP-1976-Galil #integer #on the #programming #proving #theorem proving

On Enumeration Procedures for Theorem Proving and for Integer Programming (ZG), pp. 355–381.

ICALP-1976-Schwarz #proving #reasoning #source code #termination

Event Based Reasoning — A System for Proving Correct Termination of Programs (JS), pp. 131–146.

POPL-1976-Geller #correctness #proving #testing

Test Data as an Aid in Proving Program Correctness (MMG), pp. 209–218.

ICSE-1976-MannaW #correctness #proving

Is “Sometime” Sometimes Better Than “Always”? Intermittent Assertions in Proving Program Correctness (ZM, RJW), pp. 32–39.

SOSP-J-1975-Howard76 #monitoring #proving

Proving Monitors (JHH), pp. 273–279.

STOC-1975-OppenC #data type #proving #source code

Proving Assertions about Programs that Manipulate Data Structures (DCO, SAC), pp. 107–116.

POPL-1975-Lipton #named #process #proving #reduction

Reduction: A New Method of Proving Properties of Systems of Processes (RJL), pp. 78–86.

STOC-1973-Wand

An Unusual Application of Program-Proving (MW), pp. 59–66.

POPL-1973-Morris73a #compilation #proving

Advice on Structuring Compilers and Proving Them Correct (FLM), pp. 144–152.

SIGFIDET-1972-HawryszkiewyczD #approach #correctness #database #proving

An Approach to Proving the Correctness of Data Base Operations (IH, JBD), pp. 323–348.

STOC-1971-Cook #complexity

The Complexity of Theorem-Proving Procedures (SAC), pp. 151–158.

STOC-1970-Reiter #proving #theorem proving

The Predicate Elimination Strategy in Theorem Proving (RR), pp. 180–183.