BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Used together with:
theorem (167)
program (88)
termin (65)
use (51)
correct (50)

Stem prove$ (all stems)

435 papers:

DATEDATE-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.
FMFM-2015-KroeningLW #automaton #bound #model checking #proving #safety
Proving Safety with Trace Automata and Bounded Model Checking (DK, ML, GW), pp. 325–341.
ICGTICGT-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.
SOSPSOSP-2015-HawblitzelHKLPR #distributed #named #proving
IronFleet: proving practical distributed systems correct (CH, JH, MK, JRL, BP, MLR, STVS, BZ), pp. 1–17.
CADECADE-2015-BackemanR #bound #proving #theorem proving
Theorem Proving with Bounded Rigid E-Unification (PB, PR), pp. 572–587.
CADECADE-2015-Baumgartner #named #proving #theorem proving
SMTtoTPTP — A Converter for Theorem Proving Formats (PB), pp. 285–294.
CADECADE-2015-HouGT #automation #logic #proving #theorem proving
Automated Theorem Proving for Assertions in Separation Logic with All Connectives (ZH, RG, AT), pp. 501–516.
CADECADE-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.
CAVCAV-2015-KarbyshevBIRS #invariant #proving
Property-Directed Inference of Universal Invariants or Proving Their Absence (AK, NB, SI, NR, SS), pp. 583–602.
ICLPICLP-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.
RTARTA-2015-EndrullisZ #automaton #finite #proving
Proving non-termination by finite automata (JE, HZ), pp. 160–176.
VMCAIVMCAI-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.
VMCAIVMCAI-2015-UrbanM #abstract interpretation #proving
Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation (CU, AM), pp. 190–208.
ITiCSEITiCSE-2014-MI #bound #query
A method to prove query lower bounds (JM, SI), pp. 81–86.
TACASTACAS-2014-ChenCFNO #proving #safety
Proving Nontermination via Safety (HYC, BC, CF, KN, PWO), pp. 156–171.
TACASTACAS-2014-Cheval #algorithm #equivalence #named #proving
APTE: An Algorithm for Proving Trace Equivalence (VC), pp. 587–592.
WRLAWRLA-2014-LucasM14a #2d #dependence #proving #termination
2D Dependency Pairs for Proving Operational Termination of CTRSs (SL, JM), pp. 195–212.
SASSAS-2014-UrbanM #abstract domain #proving #termination
A Decision Tree Abstract Domain for Proving Conditional Termination (CU, AM), pp. 302–318.
FLOPSFLOPS-2014-Bahr #compilation #correctness #graph #proving #using
Proving Correctness of Compilers Using Structured Graphs (PB), pp. 221–237.
DLTDLT-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.
FMFM-2014-DenmanM #automation #proving
Automated Real Proving in PVS via MetiTarski (WD, CAM), pp. 194–199.
PPDPPPDP-2014-AotoS #induction #proving #theorem
Decision Procedures for Proving Inductive Theorems without Induction (TA, SS), pp. 237–248.
PPDPPPDP-2014-LucasM #declarative #logic #proving #source code #termination
Proving Operational Termination of Declarative Programs in General Logics (SL, JM), pp. 111–122.
PPDPPPDP-2014-MehnerSSV #functional #parametricity #proving #theorem
Parametricity and Proving Free Theorems for Functional-Logic Languages (SM, DS, LS, JV), pp. 19–30.
SPLCSPLC-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.
CAVCAV-2014-LarrazNORR #proving #using
Proving Non-termination Using Max-SMT (DL, KN, AO, ERC, AR), pp. 779–796.
IJCARIJCAR-2014-BaumgartnerBW #finite #proving #quantifier #theorem proving
Finite Quantification in Hierarchic Theorem Proving (PB, JB, UW), pp. 152–167.
IJCARIJCAR-2014-BeyersdorffC #complexity #proving #theorem proving
The Complexity of Theorem Proving in Circumscription and Minimal Entailment (OB, LC), pp. 403–417.
IJCARIJCAR-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.
IJCARIJCAR-2014-NigamRL #automation #named #permutation #proving
Quati: An Automated Tool for Proving Permutation Lemmas (VN, GR, LL), pp. 255–261.
IJCARIJCAR-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.
RTARTA-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.
ASEASE-2013-HuangMM #proving #smt #using
Proving MCAPI executions are correct using SMT (YH, EM, JM), pp. 26–36.
TACASTACAS-2013-CookSZ #proving #termination
Ramsey vs. Lexicographic Termination Proving (BC, AS, FZ), pp. 47–61.
CIAACIAA-J-2012-GocHS13 #automation #combinator #word
Automatic Theorem-Proving in Combinatorics on Words (DG, DH, JS), pp. 781–798.
ICALPICALP-v1-2013-LauriaPRT #complexity #graph #proving
The Complexity of Proving That a Graph Is Ramsey (ML, PP, VR, NT), pp. 684–695.
IFMIFM-2013-AndriamiarinaMS #algorithm #distributed #modelling
Integrating Proved State-Based Models for Constructing Correct Distributed Algorithms (MBA, DM, NKS), pp. 268–284.
HILTHILT-2013-Taft #concurrent #named #parallel #proving #safety #source code #thread #tutorial
Tutorial: proving safety of parallel / multi-threaded programs (STT), pp. 1–2.
PPDPPPDP-2013-KrienerKB #coq #prolog #proving #semantics
Proofs you can believe in: proving equivalences between Prolog semantics in Coq (JK, AK, SB), pp. 37–48.
SACSAC-PL-J-2010-PopeeaC13 #analysis #debugging #proving #safety
Dual analysis for proving safety and finding bugs (CP, WNC), pp. 390–411.
CADECADE-2013-WilliamsK #problem #proving #reduction #satisfiability
Propositional Temporal Proving with Reductions to a SAT Problem (RW, BK), pp. 421–435.
CAVCAV-2013-BrockschmidtCF #proving #termination
Better Termination Proving through Cooperation (MB, BC, CF), pp. 413–429.
CAVCAV-2013-GantyG #proving #termination
Proving Termination Starting from the End (PG, SG), pp. 397–412.
CAVCAV-2013-KovacsV #first-order #proving #theorem proving
First-Order Theorem Proving and Vampire (LK, AV), pp. 1–35.
CSLCSL-2013-Kikuchi #nondeterminism #normalisation #proving #λ-calculus
Proving Strong Normalisation via Non-deterministic Translations into Klop’s Extended λ-Calculus (KK), pp. 395–414.
LICSLICS-2013-HoffmannMS #proving #reasoning
Quantitative Reasoning for Proving Lock-Freedom (JH, MM, ZS), pp. 124–133.
RTARTA-2013-WinklerZM #automation #proving #sequence #termination
Beyond Peano Arithmetic — Automatically Proving Termination of the Goodstein Sequence (SW, HZ, AM), pp. 335–351.
ICSTSAT-2013-Beyersdorff #complexity #logic #proving #theorem proving
The Complexity of Theorem Proving in Autoepistemic Logic (OB), pp. 365–376.
TLCATLCA-2013-Herbelin #proving
Proving with Side Effects (HH), p. 2.
DACDAC-2012-PurandareAH #correctness #proving #regular expression
Proving correctness of regular expression accelerators (MP, KA, CH), pp. 350–355.
TACASTACAS-2012-HolzerKSTV #contest #proving #reachability #using
Proving Reachability Using FShell — (Competition Contribution) (AH, DK, CS, MT, HV), pp. 538–541.
PLDIPLDI-2012-CarbinKMR #approximate #nondeterminism #proving #source code
Proving acceptability properties of relaxed nondeterministic approximate programs (MC, DK, SM, MCR), pp. 169–180.
CIAACIAA-2012-GocHS #automation #combinator #word
Automatic Theorem-Proving in Combinatorics on Words (DG, DH, JS), pp. 180–191.
HILTHILT-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.
HILTHILT-2012-Leino12a #proving #using #verification #why
Program proving using intermediate verification languages (IVLs) like boogie and why3 (KRML), pp. 25–26.
LOPSTRLOPSTR-2012-Seki #logic programming #program transformation #proving #source code
Proving Properties of Co-logic Programs with Negation by Program Transformations (HS), pp. 213–227.
CAVCAV-2012-EsparzaGK #probability #proving #source code #termination #using
Proving Termination of Probabilistic Programs Using Patterns (JE, AG, SK), pp. 123–138.
CAVCAV-2012-SchellhornWD #algorithm #how
How to Prove Algorithms Linearisable (GS, HW, JD), pp. 243–259.
IJCARIJCAR-2012-EmmesEG #automation #proving
Proving Non-looping Non-termination Automatically (FE, TE, JG), pp. 225–240.
LICSLICS-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.
ESOPESOP-2011-BieniusaT #memory management #proving #transaction
Proving Isolation Properties for Software Transactional Memory (AB, PT), pp. 38–56.
TACASTACAS-2011-ChamarthiDMV #proving #theorem proving
The ACL2 Sedan Theorem Proving System (HRC, PCD, PM, DV), pp. 291–295.
SEFMSEFM-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.
SEFMSEFM-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.
ICFPICFP-2011-HinzeJ #category theory #fixpoint #proving
Proving the unique fixed-point principle correct: an adventure with category theory (RH, DWHJ), pp. 359–371.
HCIHCI-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.
LOPSTRLOPSTR-2011-Seki #logic programming #proving #source code
Proving Properties of Co-Logic Programs by Unfold/Fold Transformations (HS), pp. 205–220.
SACSAC-2011-Blech #encryption #logic #proving #security
Proving the security of ElGamal encryption via indistinguishability logic (JOB), pp. 1625–1632.
ESEC-FSEESEC-FSE-2011-ChaudhuriGLN #proving #robust #source code
Proving programs robust (SC, SG, RL, SN), pp. 102–112.
CADECADE-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.
CADECADE-2011-Cook #liveness #proving #roadmap #termination
Advances in Proving Program Termination and Liveness (BC), p. 4.
CADECADE-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.
RTARTA-2011-AotoT #confluence #proving #term rewriting
A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems (TA, YT), pp. 91–106.
RTARTA-2011-NeurauterM #matrix #proving #term rewriting #termination
Revisiting Matrix Interpretations for Proving Termination of Term Rewriting (FN, AM), pp. 251–266.
RTARTA-2011-ZantemaE #automation #proving #similarity
Proving Equality of Streams Automatically (HZ, JE), pp. 393–408.
TAPTAP-2011-Gaudel #modelling #proving #source code #testing
Checking Models, Proving Programs, and Testing Systems (MCG), pp. 1–13.
VMCAIVMCAI-2011-CookFKP #biology #proving
Proving Stabilization of Biological Systems (BC, JF, EK, NP), pp. 134–149.
FASEFASE-2010-DarvasM #consistency #proving #using
Proving Consistency and Completeness of Model Classes Using Theory Interpretation (ÁD, PM), pp. 218–232.
WRLAWRLA-2010-GutierrezL #dependence #framework #proving #termination
Proving Termination in the Context-Sensitive Dependency Pair Framework (RG, SL), pp. 18–34.
FLOPSFLOPS-2010-NishidaS #injection #proving #term rewriting
Proving Injectivity of Functions via Program Inversion in Term Rewriting (NN, MS), pp. 288–303.
KEODKEOD-2010-KatsumiG #lifecycle #ontology #proving #theorem proving
Theorem Proving in the Ontology Lifecycle (MK, MG), pp. 37–49.
LOPSTRLOPSTR-2010-HerasPR #correctness #proving #set
Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System (JH, VP, JR), pp. 37–51.
PPDPPPDP-2010-Bonacina #on the #proving #theorem proving
On theorem proving for program checking: historical perspective and recent developments (MPB), pp. 1–12.
SACSAC-2010-PopeeaC #analysis #debugging #proving #safety
Dual analysis for proving safety and finding bugs (CP, WNC), pp. 2137–2143.
SACSAC-2010-VermolenHL #consistency #modelling #proving #using
Proving consistency of VDM models using HOL (SV, JH, PGL), pp. 2503–2510.
CAVCAV-2010-Vafeiadis #automation #proving
Automatically Proving Linearizability (VV), pp. 450–464.
IJCARIJCAR-2010-BaeldeMS #induction #proving #theorem proving
Focused Inductive Theorem Proving (DB, DM, ZS), pp. 278–292.
ISSTAISSTA-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.
LICSLICS-2010-Herbelin #logic #markov #principle
An Intuitionistic Logic that Proves Markov’s Principle (HH), pp. 50–56.
LICSLICS-2010-Moore #proving #theorem proving #verification
Theorem Proving for Verification: The Early Days (JSM), p. 283.
RTARTA-2010-ZantemaR #data type #infinity #proving
Proving Productivity in Infinite Data Structures (HZ, MR), pp. 401–416.
TAPTAP-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.
TAPTAP-2010-Rusu #proving #specification #theorem proving
Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications (VR), pp. 135–150.
WRLAWRLA-2008-Rodriguez09
Combining Techniques to Reduce State Space and Prove Strong Properties (DER), pp. 267–280.
FASEFASE-2009-LeinoM #consistency #proving
Proving Consistency of Pure Methods and Model Fields (KRML, RM), pp. 231–245.
PLDIPLDI-2009-KunduTL #equivalence #optimisation #proving #using
Proving optimizations correct using parameterized program equivalence (SK, ZT, SL), pp. 327–337.
SASSAS-2009-Bouissou #algorithm #correctness #implementation #proving
Proving the Correctness of the Implementation of a Control-Command Algorithm (OB), pp. 102–119.
FMFM-2009-HoenickeLPSW
It’s Doomed; We Can Prove It (JH, KRML, AP, MS, TW), pp. 338–353.
LOPSTRLOPSTR-2009-IborraNV #dependence #proving #termination
Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing (JI, NN, GV), pp. 52–66.
LOPSTRLOPSTR-2009-PilozziSB #approach #constraints #proving
A Transformational Approach for Proving Properties of the CHR Constraint Store (PP, TS, MB), pp. 22–36.
POPLPOPL-2009-GotsmanCPV #algorithm #proving
Proving that non-blocking algorithms don’t block (AG, BC, MJP, VV), pp. 16–28.
CADECADE-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.
CADECADE-2009-McLaughlinP #performance #proving #theorem proving
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method (SM, FP), pp. 230–244.
CADECADE-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.
CADECADE-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.
CAVCAV-2009-Strichman #equivalence #proving #source code #verification
Regression Verification: Proving the Equivalence of Similar Programs (OS), p. 63.
ICLPICLP-2009-PilozziS #proving #termination
Proving Termination by Invariance Relations (PP, DDS), pp. 499–503.
ICSTICST-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.
RTARTA-2009-AotoYT #automation #confluence #proving #term rewriting
Proving Confluence of Term Rewriting Systems Automatically (TA, JY, YT), pp. 93–102.
RTARTA-2009-FuhsGPSF #integer #proving #term rewriting #termination
Proving Termination of Integer Term Rewriting (CF, JG, MP, PSK, SF), pp. 32–47.
ICSTSAT-2009-BeyersdorffM #question
Does Advice Help to Prove Propositional Tautologies? (OB, SM), pp. 65–72.
TACASTACAS-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.
PEPMPEPM-2008-Voigtlander #correctness #proving #theorem
Proving correctness via free theorems: the case of the destroy/build-rule (JV), pp. 13–20.
SASSAS-2008-ConwayDNB #analysis #fault #pointer #proving
Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors (CLC, DD, KSN, CB), pp. 62–77.
FLOPSFLOPS-2008-PrinceGM #proving #using
Proving Properties about Lists Using Containers (RP, NG, CM), pp. 97–112.
DLTDLT-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.
LATALATA-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-VCGT-VC-2007-Bruggink08 #graph transformation #proving #termination #towards
Towards a Systematic Method for Proving Termination of Graph Transformation Systems (HJSB), pp. 23–38.
ICGTICGT-2008-Pennemann #proving #theorem proving
Resolution-Like Theorem Proving for High-Level Conditions (KHP), pp. 289–304.
KRKR-2008-Lin #proving
Proving Goal Achievability (FL), pp. 621–628.
POPLPOPL-2008-GuptaHMRX #proving
Proving non-termination (AG, TAH, RM, AR, RGX), pp. 147–158.
CAVCAV-2008-CookGLRS #proving #termination
Proving Conditional Termination (BC, SG, TLA, AR, MS), pp. 328–340.
CAVCAV-2008-Harrison #proving #theorem proving #tutorial #verification
Theorem Proving for Verification (Invited Tutorial) (JH), pp. 11–18.
CAVCAV-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.
CSLCSL-2008-Nguyen #proving #using
Proving Infinitude of Prime Numbers Using Binomial Coefficients (PN), pp. 184–198.
IJCARIJCAR-2008-KremerMT #protocol #proving
Proving Group Protocols Secure Against Eavesdroppers (SK, AM, RT), pp. 116–131.
IJCARIJCAR-2008-Melquiond #bound #proving
Proving Bounds on Real-Valued Functions with Computations (GM), pp. 2–17.
IJCARIJCAR-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.
RTARTA-2008-MoserS #polynomial #proving #using
Proving Quadratic Derivational Complexities Using Context Dependent Interpretations (GM, AS), pp. 276–290.
PLDIPLDI-2007-CookPR #concurrent #proving #termination #thread
Proving thread termination (BC, AP, AR), pp. 320–330.
IFMIFM-2007-DerrickSW #proving #refinement
Proving Linearizability Via Non-atomic Refinement (JD, GS, HW), pp. 195–214.
SEFMSEFM-2007-BabicHRC #proving #termination
Proving Termination by Divergence (DB, AJH, ZR, BC), pp. 93–102.
SEFMSEFM-2007-Cook #automation #concurrent #proving #source code
Automatically Proving Concurrent Programs Correct (BC), pp. 269–272.
CEFPCEFP-2007-MolEP #functional #lazy evaluation #proving #source code
Proving Properties of Lazy Functional Programs with Sparkle (MdM, MCJDvE, RP), pp. 41–86.
LOPSTRLOPSTR-2007-Codish #proving #termination
Proving Termination with (Boolean) Satisfaction (MC), pp. 1–7.
POPLPOPL-2007-CookGPRV #proving #source code
Proving that programs eventually do something good (BC, AG, AP, AR, MYV), pp. 265–276.
CADECADE-2007-GieslTSS #bound #proving #termination
Proving Termination by Bounded Increase (JG, RT, SS, PSK), pp. 443–459.
CADECADE-2007-TiwariG #logic #program analysis #proving #theorem proving #using
Logical Interpretation: Static Program Analysis Using Theorem Proving (AT, SG), pp. 147–166.
CAVCAV-2007-Cook #automation #proving #termination
Automatically Proving Program Termination (BC), p. 1.
LICSLICS-2007-NguyenC #complexity #proving #theorem
The Complexity of Proving the Discrete Jordan Curve Theorem (PN, SAC), pp. 245–256.
RTARTA-2007-KorpM #bound #proving #term rewriting #termination #using
Proving Termination of Rewrite Systems Using Bounds (MK, AM), pp. 273–287.
TAPTAP-2007-Haiyan #algorithm #distributed #proving #testing #type system
Testing and Proving Distributed Algorithms in Constructive Type Theory (QH), pp. 79–94.
TAPTAP-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.
DACDAC-2006-AwedhS #automation #bound #invariant #model checking
Automatic invariant strengthening to prove properties in bounded model checking (MA, FS), pp. 1073–1076.
DATEDATE-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.
SASSAS-2006-Bertrane #communication #proving
Proving the Properties of Communicating Imperfectly-Clocked Synchronous Systems (JB), pp. 370–386.
FMFM-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.
SFMSFM-2006-Harrison #float #proving #theorem proving #using #verification
Floating-Point Verification Using Theorem Proving (JH), pp. 211–242.
SFMSFM-2006-Manolios #proving #refinement #theorem proving
Refinement and Theorem Proving (PM), pp. 176–210.
IFLIFL-2006-Kozsik #proving #type system
Proving Program Properties Specified with Subtype Marks (TK), pp. 163–180.
LOPSTRLOPSTR-2006-NguyenS #automation #named #polynomial #proving #termination
Polytool: Proving Termination Automatically Based on Polynomial Interpretations (MTN, DDS), pp. 210–218.
RERE-2006-Miller #development #modelling #proving #requirements
Proving the Shalls: Requirements, Proofs, and Model-Based Development (SPM), p. 261.
ICSEICSE-2006-ManoliosV #proving #static analysis #termination #theorem proving
Integrating static analysis and general-purpose theorem proving for termination analysis (PM, DV), pp. 873–876.
PPoPPPPoPP-2006-VafeiadisHHS #correctness #proving
Proving correctness of highly-concurrent linearisable objects (VV, MH, CARH, MS), pp. 129–136.
ICLPICLP-2006-PettorossiPS #constraints #logic programming #proving #source code
Proving Properties of Constraint Logic Programs by Eliminating Existential Variables (AP, MP, VS), pp. 179–195.
IJCARIJCAR-2006-EndrullisWZ #matrix #proving #term rewriting #termination
Matrix Interpretations for Proving Termination of Term Rewriting (JE, JW, HZ), pp. 574–588.
IJCARIJCAR-2006-Mahboubi #algorithm #implementation #performance #proving
Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials (AM), pp. 438–452.
ISSTAISSTA-2006-YorshBS #abstraction #exclamation #proving #testing #theorem proving
Testing, abstraction, theorem proving: better together! (GY, TB, MS), pp. 145–156.
RTARTA-2006-BournezG #proving #termination
Proving Positive Almost Sure Termination Under Strategies (OB, FG), pp. 357–371.
RTARTA-2006-Koprowski06a #automation #named #termination
TPA: Termination Proved Automatically (AK), pp. 257–266.
ASEASE-2005-GheyiMB #approach #proving #refactoring
A rigorous approach for proving model refactorings (RG, TM, PB), pp. 372–375.
DACDAC-2005-MonyBPK #proving
Exploiting suspected redundancy without proving it (HM, JB, VP, RK), pp. 463–466.
WRLAWRLA-2004-PalominoP05 #maude #model checking #proving
Proving VLRL Action Properties with the Maude Model Checker (MP, IP), pp. 113–133.
SEFMSEFM-2005-OlssonW #correctness #imperative #induction #proving #source code
Customised Induction Rules for Proving Correctness of Imperative Programs (OO, AW), pp. 180–189.
SEFMSEFM-2005-Trentelman #correctness #proving #using
Proving Correctness of JavaCard DL Taclets using Bali (KT), pp. 160–169.
ICFPICFP-2005-ChenX #programming #proving #theorem proving
Combining programming with theorem proving (CC, HX), pp. 66–77.
AdaEuropeAdaEurope-2005-SwardB #equivalence #functional #proving #slicing
Proving Functional Equivalence for Program Slicing in SPARK™ (RES, LCBI), pp. 105–114.
CADECADE-2005-OgawaHO #incremental #proving
Proving Properties of Incremental Merkle Trees (MO, EH, SO), pp. 424–440.
CAVCAV-2005-CookKS #named #proving #theorem proving #verification
Cogent: Accurate Theorem Proving for Program Verification (BC, DK, NS), pp. 296–300.
RTARTA-2005-BournezG #proving #termination
Proving Positive Almost-Sure Termination (OB, FG), pp. 323–337.
VMCAIVMCAI-2005-Cousot #abstraction #parametricity #programming #proving #termination
Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming (PC), pp. 1–24.
FoSSaCSFoSSaCS-2004-Lucas #proving #termination
Polynomials for Proving Termination of Context-Sensitive Rewriting (SL), pp. 318–332.
PEPMPEPM-2004-DuranLMMU #equation #proving #source code #termination
Proving termination of membership equational programs (FD, SL, JM, CM, XU), pp. 147–158.
IFMIFM-2004-EllisI #automation #integration #program analysis #proving #theorem proving
An Integration of Program Analysis and Automated Theorem Proving (BJE, AI), pp. 67–86.
IFMIFM-2004-Melham #functional #model checking #proving #theorem proving
Integrating Model Checking and Theorem Proving in a Reflective Functional Language (TFM), pp. 36–39.
ICEISICEIS-v1-2004-Augusto #model checking #theorem proving #verification
Model Checking and Theorem Proving-Based Verification of EIS (JCA), p. XXXIII-XXXIV.
LOPSTRPDCL-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.
CAVCAV-2004-AwedhS #bound #model checking #proving
Proving More Properties with Bounded Model Checking (MA, FS), pp. 96–108.
CAVCAV-2004-BallCLZ #abstraction #automation #named #proving #refinement #theorem proving
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement (TB, BC, SKL, LZ), pp. 457–461.
CSLCSL-2004-GanzingerK #equation #proving #reasoning #theorem proving
Integrating Equational Reasoning into Instantiation-Based Theorem Proving (HG, KK), pp. 71–84.
CSLCSL-2004-GiacobazziM #proving
Proving Abstract Non-interference (RG, IM), pp. 280–294.
CSLCSL-2004-Lynch #proving #theorem proving
Unsound Theorem Proving (CL), pp. 473–487.
LICSLICS-2004-Leivant #logic #proving #termination
Proving Termination Assertions in Dynamic Logics (DL), pp. 89–98.
RTARTA-2004-LimetS #logic programming #proving #source code #term rewriting
Proving Properties of Term Rewrite Systems via Logic Programs (SL, GS), pp. 170–184.
RTARTA-2004-Lucas #named #proving #termination
mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting (SL), pp. 200–209.
RTARTA-2004-Zantema #automation #named #termination
TORPA: Termination of Rewriting Proved Automatically (HZ), pp. 95–104.
DACDAC-2003-GuptaRSBBFPOS #verification
Formal verification — prove it or pitch it (RKG, SR, SKS, BB, DKB, MF, CP, JO, FS), pp. 710–711.
TACASTACAS-2003-Lee #case study #experience #what
What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code (PL0), p. 1.
PLDIPLDI-2003-LernerMC #automation #compilation #correctness #optimisation #proving
Automatically proving the correctness of compiler optimizations (SL, TDM, CC), pp. 220–231.
STOCSTOC-2003-KabanetsI #bound #polynomial #proving #testing
Derandomizing polynomial identity tests means proving circuit lower bounds (VK, RI), pp. 355–364.
FMFME-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.
FMFME-2003-MillerTH #proving
Proving the Shalls (SPM, ACT, MPEH), pp. 75–93.
SEFMSEFM-2003-DeharbeR #debugging #proving #theorem proving #verification
Light-Weight Theorem Proving for Debugging and Verifying Units of Code (DD, SR), pp. 220–228.
LOPSTRLOPSTR-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.
LOPSTRLOPSTR-2003-SerebrenikS #proving #termination
Proving Termination with Adornments (AS, DDS), pp. 108–109.
CADECADE-2003-AvenhausKSW #exclamation #how #induction #theorem
How to Prove Inductive Theorems? QUODLIBET! (JA, UK, TSS, CPW), pp. 328–333.
CADECADE-2003-MehtaN #higher-order #logic #pointer #proving #source code
Proving Pointer Programs in Higher-Order Logic (FM, TN), pp. 121–135.
CAVCAV-2003-FlanaganJOS #lazy evaluation #proving #theorem proving #using
Theorem Proving Using Lazy Proof Explication (CF, RJ, XO, JBS), pp. 355–367.
FATESFATES-2003-HahnleW #proving #testing #theorem proving #using
Using a Software Testing Technique to Improve Theorem Proving (RH, AW), pp. 30–41.
LICSLICS-2003-GanzingerK #proving #theorem proving
New Directions in Instantiation-Based Theorem Proving (HG, KK), pp. 55–64.
FoSSaCSFoSSaCS-2002-BoerGM #concurrent #constraints #correctness #proving #source code
Proving Correctness of Timed Concurrent Constraint Programs (FSdB, MG, MCM), pp. 37–51.
FoSSaCSFoSSaCS-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.
SASSAS-2002-VeldhuizenL #compilation #optimisation #proving
Guaranteed Optimization: Proving Nullspace Properties of Compilers (TLV, AL), pp. 263–277.
IFLIFL-2002-DowseSB #haskell #proving
Proving Make Correct: I/O Proofs in Haskell and Clean (MD, GS, AB), pp. 68–83.
ICEISICEIS-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.
POPLPOPL-2002-LaceyJWF #compilation #correctness #logic #optimisation #proving
Proving correctness of compiler optimizations by temporal logic (DL, NDJ, EVW, CCF), pp. 283–294.
CADECADE-2002-Brown #higher-order #proving #set #theorem proving
Solving for Set Variables in Higher-Order Theorem Proving (CEB), pp. 408–422.
CADECADE-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.
CAVCAV-2002-BlomP #confluence #proving #reduction
State Space Reduction by Proving Confluence (SB, JvdP), pp. 596–609.
CAVCAV-2002-ColonS #proving #termination
Practical Methods for Proving Program Termination (MC, HS), pp. 442–454.
CAVCAV-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.
ICLPICLP-2002-Craciunescu #equivalence #proving #source code
Proving the Equivalence of CLP Programs (SC), pp. 287–301.
ISSTAISSTA-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.
ICTSSTestCom-2002-CastanetR #analysis #proving #reachability #testing #theorem proving
Generate Certified Test Cases by Combining Theorem Proving and Reachability Analysis (RC, DR), pp. 249–266.
VMCAIVMCAI-2002-GenaimCGL #termination
Combining Norms to Prove Termination (SG, MC, JPG, VL), pp. 126–138.
FASEFASE-2001-InverardiU #component #concurrent #programming #proving
Proving Deadlock Freedom in Component-Based Programming (PI, SU), pp. 60–75.
FLOPSFLOPS-J2-1998-Sakurai01 #category theory #proving
Categorical Model Construction for Proving Syntactic Properties (TS), pp. 213–244.
FLOPSFLOPS-2001-PolakovY #exception #framework #logic #order #proving
Proving Syntactic Properties of Exceptions in an Ordered Logical Framework (JP, KY), pp. 61–77.
IFLIFL-2001-ButterfieldS #comparison #correctness #paradigm #proving #source code
Proving Correctness of Programs with IO — A Paradigm Comparison (AB, GS), pp. 72–87.
IFLIFL-2001-EncinaP #correctness #proving
Proving the Correctness of the STG Machine (AdlE, RP), pp. 88–104.
IFLIFL-2001-MolEP #functional #proving #theorem proving
Theorem Proving for Functional Programmers (MdM, MCJDvE, MJP), pp. 55–71.
GPCESAIG-2001-Johann
Short Cut Fusion: Proved and Improved (PJ), pp. 47–71.
ICLPICLP-2001-DrabentM #approach #correctness #declarative #proving #source code
Proving Correctness and Completeness of Normal Programs — A Declarative Approach (WD, MM), pp. 284–299.
IJCARIJCAR-2001-NieuwenhuisHRV #evaluation #on the #proving #theorem proving
On the Evaluation of Indexing Techniques for Theorem Proving (RN, TH, AR, AV), pp. 257–271.
IJCARIJCAR-2001-SchmittLKN #interactive #proving #theorem proving
JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants (SS, LL, CK, AN), pp. 421–426.
RTARTA-2001-Barendregt #proving
Computing and Proving (HB), p. 1.
ICSTSAT-2001-Goldberg #proving #satisfiability
Proving unsatisfiability of CNFs locally (EG), pp. 96–114.
ICSTSAT-2001-McllraithA #proving #theorem proving
Theorem Proving with Structured Theories (Preliminary Report)* (SM, EA), pp. 311–328.
UMLUML-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.
CADECADE-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.
CADECADE-2000-AndrewsBB #proving #theorem proving #type system
System Description: TPS: A Theorem Proving System for Type Theory (PBA, MB, CEB), pp. 164–169.
CADECADE-2000-Harrison #proving #theorem proving #using #verification
High-Level Verification Using Theorem Proving and Formalized Mathematics (JH), pp. 1–6.
CADECADE-2000-Seger #float #model checking #proving #theorem proving
Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice (CJHS), p. 235.
ICLPCL-2000-HahnleHS #constraints #finite #generative #proving #theorem proving
Moder Generation Theorem Proving with Finite Interval Constraints (RH, RH, YS), pp. 285–299.
ICLPCL-2000-Lopez-FraguasH #functional #logic programming #proving #source code
Proving Failure in Functional Logic Programs (FJLF, JSH), pp. 179–193.
LICSLICS-2000-McMillan #model checking #proving #theorem
Some Strategies for Proving Theorems with a Model Checker (KLM), pp. 305–306.
LICSLICS-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.
FASEFASE-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.
TACASTACAS-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.
TACASTACAS-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.
FMFM-v2-1999-Nadjm-TehraniA #design #modelling #proving #theorem proving
Combining Theorem Proving and Continuous Models in Synchronous Design (SNT, ), pp. 1384–1399.
CADECADE-1999-Artemov #on the #proving #theorem proving #verification
On Explicit Reflection in Theorem Proving and Formal Verification (SNA), pp. 267–281.
CADECADE-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.
CADECADE-1999-Hickey #distributed #fault tolerance #proving #theorem proving
Fault-Tolerant Distributed Theorem Proving (JH), pp. 227–231.
CAVCAV-1999-ManoliosNS #bisimulation #model checking #proving #theorem proving
Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation (PM, KSN, RS), pp. 369–379.
CAVCAV-1999-SaidiS
Abstract and Model Check While You Prove (HS, NS), pp. 443–454.
CSLCSL-1999-Howe #interactive #proving #theorem proving #type system #using
Interactive Theorem Proving Using Type Theory (DJH), p. 578.
ICLPICLP-1999-Smaus #logic programming #proving #source code #termination
Proving Termination of Input-Consuming Logic Programs (JGS), pp. 335–349.
LICSLICS-1999-Paulson #protocol #proving #security
Proving Security Protocols Correct (LCP), pp. 370–381.
DACDAC-1998-AagaardJS #evaluation #industrial #proving #theorem proving
Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment (MA, RBJ, CJHS), pp. 538–541.
WRLAWRLA-1998-CarabettaDG #logic #semantics
CCS semantics via proved transition systems and rewriting logic (GC, PD, FG), pp. 369–387.
FLOPSFLOPS-1998-Sakurai #proving
Categorial Model Construction for Proving Syntactic Properties (TS), pp. 187–206.
ICALPICALP-1998-Lugiez #automaton #induction #proving #theorem proving
A Good Class of Tree Automata and Application to Inductive Theorem Proving (DL), pp. 409–420.
CIAAWIA-1998-LHerPM #automaton #proving #source code #using
Proving Sequential Function Chart Programs Using Automata (DL, PLP, LM), pp. 149–163.
FMFM-1998-GoerigkH #compilation #correctness #how #implementation
Rigorous Compiler Implementation Correctness: How to Prove the Real Thing Correct (WG, UH), pp. 122–136.
CADECADE-1998-FeveW #algebra #geometry #proving #theorem #using
Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules (SF, DW), pp. 17–31.
CADECADE-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.
CADECADE-1998-SchurmannP #automation #logic #proving #theorem proving
Automated Theorem Proving in a Simple Meta-Logic for LF (CS, FP), pp. 286–300.
CAVCAV-1998-Camilleri #design #multi #proving #theorem proving
A Role for Theorem Proving in Multi-Processor Design (AJC), pp. 45–48.
SASSAS-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.
FMFME-1997-AgerholmF #automation #proving #theorem proving #towards
Towards an Integrated CASE and Theorem Proving Tool for VDM-SL (SA, JF), pp. 278–297.
FMFME-1997-Stringer-CalvertSW #case study #refinement #using
Using PVS to Prove a Z Refinement: A Case Study (DWJSC, SS, IW), pp. 573–588.
CADECADE-1997-DahnGHW #automation #integration #interactive #proving #theorem proving
Integration of Automated and Interactive Theorem Proving in ILP (BID, JG, TH, AW), pp. 57–60.
CADECADE-1997-FeltyH #hybrid #interactive #proving #theorem proving #using
Hybrid Interactive Theorem Proving Using Nuprl and HOL (APF, DJH), pp. 351–365.
CADECADE-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.
CADECADE-1997-ReifSS #correctness #proving
Proving System Correctness with KIV 3.0 (WR, GS, KS), pp. 69–72.
RTARTA-1997-ArtsG #automation #normalisation #proving
Proving Innermost Normalisation Automatically (TA, JG), pp. 157–171.
RTARTA-1997-KapurS #order #proving #term rewriting #termination
A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems (DK, GS), pp. 142–156.
RTARTA-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.
TLCATLCA-1997-Ruess #calculus #proving #theorem proving
Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving (HR), pp. 319–335.
TACASTACAS-1996-Saidi #automation #concurrent #proving
A Tool for Proving Invariance Properties of Concurrent Systems Automatically (HS), pp. 412–416.
SASSAS-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.
ICALPICALP-1996-Ganzinger #proving #theorem proving
Saturation-Based Theorem Proving (Abstract) (HG), pp. 1–3.
FMFME-1996-HavelundS #model checking #protocol #proving #theorem proving #verification
Experiments in Theorem Proving and Model Checking for Protocol Verification (KH, NS), pp. 662–681.
POPLPOPL-1996-HughesPS #correctness #proving #using
Proving the Correctness of Reactive Systems Using Sized Types (JH, LP, AS), pp. 410–423.
CADECADE-1996-DenzingerS #learning #proving #theorem proving
Learning Domain Knowledge to Improve Theorem Proving (JD, SS), pp. 62–76.
CADECADE-1996-Ganzinger #proving #theorem proving
Saturation-Based Theorem Proving: Past Successes and Future Potential (Abstract) (HG), p. 1.
CADECADE-1996-GanzingerW #monad #proving #theorem proving
Theorem Proving in Cancellative Abelian Monoids (Extended Abstract) (HG, UW), pp. 388–402.
CADECADE-1996-KolbeW #proving #reuse #termination #theorem proving
Termination of Theorem Proving by Reuse (TK, CW), pp. 106–120.
CADECADE-1996-Luz-Filho #logic #proving #specification #theorem proving
Grammar Specification in Categorial Logics and Theorem Proving (SFLF), pp. 703–717.
CADECADE-1996-Martin #proving #theorem proving
Theorem Proving with Group Presentations: Examples and Questions (UM), pp. 358–372.
CADECADE-1996-MelisW #proving #theorem proving
Internal Analogy in Theorem Proving (EM, JW), pp. 92–105.
CAVCAV-1996-ClarkeGZ #algorithm #proving #theorem proving #using #verification
Verifying the SRT Division Algorithm Using Theorem Proving Techniques (EMC, SMG, XZ), pp. 111–122.
CAVCAV-1996-GrafS #invariant #proving #theorem proving #using #verification
Verifying Invariants Using theorem Proving (SG, HS), pp. 196–207.
ICLPJICSLP-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.
RTARTA-1996-BoudetCM #proving #theorem proving #unification
AC-Complete Unification and its Application to Theorem Proving (AB, EC, CM), pp. 18–32.
RTARTA-1996-Gramlich #on the #proving #termination
On Proving Termination by Innermost Termination (BG), pp. 93–107.
RTARTA-1996-HillenbrandBF #on the #performance #proving #theorem proving
On Gaining Efficiency in Completion-Based Theorem Proving (TH, AB, RF), pp. 432–435.
RTARTA-1996-Stuber #integer #proving #theorem proving
Superposition Theorem Proving for Albelian Groups Represented as Integer Modules (JS), pp. 33–47.
PEPMPEPM-1995-Metayer #data type #proving #recursion #source code
Proving Properties of Programs Defined over Recursive Data Structures (DLM), pp. 88–99.
LOPSTRLOPSTR-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.
SACSAC-1995-Bsaies #logic programming #proving
Discovering and proving logic program properties (KB), pp. 369–373.
CAVCAV-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.
ICLPICLP-1995-Hirata #correctness #haskell #proving #π-calculus
Proving Correctness of Translation from Moded Flat GHC to π-Calculus (KH), p. 818.
ICLPILPS-1995-MarchioriT #logic programming #proving #source code #termination
Proving Termination of Logic Programs with Delay Declarations (EM, FT), pp. 447–461.
RTARTA-1995-Kuper #proving #reduction
Proving the Genericity Lemma by Leftmost Reduction is Simple (JK), pp. 271–278.
RTARTA-1995-Stickel #proving #term rewriting #theorem proving
Term Rewriting in Contemporary Resolution Theorem Proving (Abstract) (MES), p. 101.
PPDPALP-1994-BidoitH #behaviour #first-order #logic #proving #standard #theorem
Proving Behavioural Theorems with Standard First-Order Logic (MB, RH), pp. 41–58.
PPDPALP-1994-CodishM #algebra #approximate #proving
Proving Implications by Algebraic Approximation (MC, GM), pp. 6–22.
POPLPOPL-1994-BoerGMP #concurrent #constraints #proving #source code
Proving Concurrent Constraint Programs Correct (FSdB, MG, EM, CP), pp. 98–108.
CADECADE-1994-BeckertP #agile #named #proving #theorem proving
leanTAP: Lean Tableau-Based Theorem Proving (Extended Abstract) (BB, JP), pp. 793–797.
CADECADE-1994-BonacinaM #distributed #proving #theorem proving
Distributed Theorem Proving by Peers (MPB, WM), pp. 841–845.
CADECADE-1994-ChuP #first-order #proving #semantics #theorem proving #using
Semantically Guided First-Order Theorem Proving using Hyper-Linking (HC, DAP), pp. 192–206.
CADECADE-1994-ClarkeZ #problem #proving #symbolic computation #theorem proving
Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan (EMC, XZ), pp. 758–763.
CADECADE-1994-FeltyH #proving #theorem proving
Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables (APF, DJH), pp. 605–619.
CADECADE-1994-Goubault #proving
Proving with BDDs and Control of Information (JG), pp. 499–513.
CADECADE-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.
CADECADE-1994-Plaisted #performance #proving #theorem proving
The Search Efficiency of Theorem Proving Strategies (DAP), pp. 57–71.
CADECADE-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.
CADECADE-1994-Wang #algebra #geometry #proving
Algebraic Factoring and Geometry Proving (DW), pp. 386–400.
ICLPICLP-1994-BreuerSK #design #hardware #proving
Proving Hardware Designs (PTB, LS, CDK), p. 745.
DACDAC-1993-JoyceS #evaluation #interactive #symbolic computation
Linking BDD-Based Symbolic Evaluation to Interactive Theorem-Proving (JJJ, CJHS), pp. 469–474.
PPDPPLILP-1993-BurnM #analysis #compilation #correctness #optimisation #proving #strict
Proving the Correctness of Compiler Optimizations Based on Strictness Analysis (GLB, DLM), pp. 346–364.
CAVCAV-1993-Hungar #model checking #parallel #process #proving #theorem proving #verification
Combining Model Checking and Theorem Proving to Verify Parallel Processes (HH), pp. 154–165.
ICLPICLP-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.
ICLPICLP-1993-RaoKS #haskell #proving #source code #termination
Proving Termination of GHC Programs (MRKKR, DK, RKS), pp. 720–736.
ICLPILPS-1993-KirschenbaumS #prolog #proving #source code
Enhancement Structures for Proving Prolog Programs Correct (MK, LS), p. 631.
RTARTA-1993-AvenhausD #equation #proving #theorem proving
Distributing Equational Theorem Proving (JA, JD), pp. 62–76.
RTARTA-1993-Bachmair #proving #theorem proving
Rewrite Techniques in Theorem Proving (Abstract) (LB), p. 1.
RTARTA-1993-Gallier #proving
Proving Properties of Typed λ Terms: Realizability, Covers, and Sheaves (Abstract) (JHG), p. 136.
ESOPESOP-1992-BernsteinRS #proving #safety
Proving Safety of Speculative Load Instructions at Compile Time (DB, MR, SS), pp. 56–72.
ESOPESOP-1992-Gnaedig #proving #specification #theorem proving
ELIOS-OBJ Theorem Proving in a Specification Language (IG), pp. 182–199.
ICALPICALP-1992-DeganoP
Proved Trees (PD, CP), pp. 629–640.
LISPLFP-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.
LISPLFP-1992-WandO #correctness #proving
Proving the Correctness of Storage Representations (MW, DO), pp. 151–160.
PPDPALP-1992-BachmairGW #first-order #proving #theorem proving
Theorem Proving for Hierarchic First-Order Theories (LB, HG, UW), pp. 420–434.
CADECADE-1992-AlexanderP #proving #similarity #theorem
Proving Equality Theorems with Hyper-Linking (GDA, DAP), pp. 706–710.
CADECADE-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.
CADECADE-1992-ChouG #geometry #proving
Proving Geometry Statements of Constructive Type (SCC, XSG), pp. 20–34.
CADECADE-1992-Dafa #automation #deduction #proving #theorem proving
A Natural Deduction Automated Theorem Proving System (LD), pp. 668–672.
CADECADE-1992-NieuwenhuisR #proving #theorem proving
Theorem Proving with Ordering Constrained Clauses (RN, AR), pp. 477–491.
CADECADE-1992-Voronkov #logic #proving #standard #theorem proving
Theorem Proving in Non-Standard Logics Based on the Inverse Method (AV), pp. 648–662.
CADECADE-1992-ZhangH #induction #proving #set #theorem
Proving the Chinese Remainder Theorem by the Cover Set Induction (HZ, XH), pp. 431–445.
CSLCSL-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.
ICLPJICSLP-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.
FMVDME-1991-1-Clement #development
Combining Transformation and Posit-and Prove in a VDM Development (TC), pp. 63–80.
KRKR-1991-HalpernV #model checking #proving #theorem proving
Model Checking vs. Theorem Proving: A Manifesto (JYH, MYV), pp. 325–334.
CAVCAV-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.
CSLCSL-1991-RaoKS #logic programming #proving #source code #termination
A Transformational Methodology for Proving Termination of Logic Programs (MRKKR, DK, RKS), pp. 213–226.
CSLCSL-1991-Weiermann #proving #term rewriting #termination
Proving Termination for Term Rewriting Systems (AW), pp. 419–428.
ICLPICLP-1991-ColussiM #axiom #correctness #logic programming #proving #semantics #source code #using
Proving Correctness of Logic Programs Using Axiomatic Semantics (LC, EM), pp. 629–642.
ICLPICLP-1991-Hagiya #higher-order #proving #theorem proving #unification
Higher-Order Unification as a Theorem Proving Procedure (MH), pp. 270–284.
ICLPICLP-1991-Lever #proving
Proving Program Properties by Means of SLS-Resolution (JML), pp. 614–628.
LICSLICS-1991-HuttelS #process #proving #similarity #word
Actions Speak Louder than Words: Proving Bisimilarity for Context-Free Processes (HH, CS), pp. 376–386.
LICSLICS-1991-PeledKP #logic #proving #specification
Specifying and Proving Serializability in Temporal Logic (DP, SK, AP), pp. 232–244.
RTARTA-1991-Avenhaus #equation #induction #proving #theorem
Proving Equational and Inductive Theorems by Completion and Embedding Techniques (JA), pp. 361–373.
RTARTA-1991-BonacinaH #on the #proving #theorem proving
On Fairness of Completion-Based Theorem Proving Strategies (MPB, JH), pp. 348–360.
RTARTA-1991-Hermann #on the #proving
On Proving Properties of Completion Strategies (MH), pp. 398–410.
ICALPICALP-1990-PeledP #liveness #partial order #proving
Proving Partial Order Liveness Properties (DP, AP), pp. 553–571.
PPDPALP-1990-Farres-Casals #correctness #proving #specification
Proving Correctness wrt Specifications with Hidden Parts (JFC), pp. 25–39.
PPDPALP-1990-Goguen #proving
Proving and Rewriting (JAG), pp. 1–24.
CADECADE-1990-AndrewsINP #proving #theorem proving
The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 641–642.
CADECADE-1990-ChouG #algorithm #composition #geometry #proving #theorem proving
Ritt-Wu’s Decomposition Algorithm and Geometry Theorem Proving (SCC, XSG), pp. 207–220.
CADECADE-1990-CostaHLS #automation #implementation #logic #proving #theorem proving
Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation (NCAdC, LJH, JJL, VSS), pp. 72–86.
CADECADE-1990-Hagiya #higher-order #programming #proving #unification #using
Programming by Example and Proving by Example Using Higher-order Unification (MH), pp. 588–602.
CADECADE-1990-HeiselRS #proving #theorem proving #verification
Tactical Theorem Proving in Program Verification (MH, WR, WS), pp. 117–131.
CADECADE-1990-HsiangJ #proving #theorem proving #tutorial
Tutorial on Rewrite-Based Theorem Proving (JH, JPJ), p. 684.
CADECADE-1990-LuskM #automation #proving #theorem proving #tutorial
Tutorial on High-Performance Automated Theorem Proving (ELL, WM), p. 681.
CADECADE-1990-Tuominen #framework #logic #proving #theorem proving
Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic (HT), pp. 514–527.
SEKESEKE-1989-Cooke #design #proving
Proving Properties of Software Design Methods (DEC), pp. 9–12.
DACDAC-1988-MadreB #behaviour #comparison #correctness #proving #using
Proving Circuit Correctness Using Formal Comparison Between Expected and Extracted Behaviour (JCM, JPB), pp. 205–210.
ICALPICALP-1988-Culik #decidability #equivalence #problem #proving
New Techniques for Proving the Decidability of Equivalence Problems (KCI), pp. 162–175.
FMVDME-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.
PPDPALP-1988-HofbauerK #induction #proving #term rewriting #theorem
Proving Inductive Theorems Based on Term Rewriting Systems (DH, RDK), pp. 180–190.
CADECADE-1988-AndrewsINP #proving #theorem proving
The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 760–761.
CADECADE-1988-Hines #knowledge-based #proving #theorem proving
Hyper-Chaining and Knowledge-Based Theorem Proving (LMH), pp. 469–486.
CADECADE-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.
CADECADE-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.
CADECADE-1988-ZhangK #first-order #proving #theorem proving #using
First-Order Theorem Proving Using Conditional Rewrite Rules (HZ, DK), pp. 1–20.
CSLCSL-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.
LICSLICS-1988-Baudinet #approach #prolog #proving #semantics #source code #termination
Proving Termination Properties of Prolog Programs: A Semantic Approach (MB), pp. 336–347.
LICSLICS-1988-Tiomkin #proving
Proving unprovability (MLT), pp. 22–26.
CSLCSL-1987-BryM #database #deduction #finite #proving #satisfiability
Proving Finite Satisfiability of Deductive Databases (FB, RM), pp. 44–55.
CSLCSL-1987-Schoning #complexity
Complexity Cores and Hard-To-Prove Formulas (US), pp. 273–280.
LICSLICS-1987-AlpernS #proving
Proving Boolean Combinations of Deterministic Properties (BA, FBS), pp. 131–137.
LICSLICS-1987-BachmairD #first-order #proving #theorem proving
Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.
LICSLICS-1987-GallierRS #equation #proving #theorem proving #using
Theorem Proving Using Rigid E-Unification Equational Matings (JHG, SR, WS), pp. 338–346.
ESOPESOP-1986-Stark #concept #proving #specification
Proving Entailment Between Conceptual State Specifications (EWS), pp. 197–209.
CADECADE-1986-AbadiM #proving #theorem proving
Modal Theorem Proving (MA, ZM), pp. 172–189.
CADECADE-1986-AndrewsPIK #proving #theorem proving
The TPS Theorem Proving System (PBA, FP, SI, CPK), pp. 663–664.
CADECADE-1986-BeierleOV #automation #proving #theorem proving
Automatic Theorem Proving in the ISDV System (CB, WGO, AV), pp. 670–671.
CADECADE-1986-BiundoHHW #induction #proving #theorem proving
The Karlsruhe Induction Theorem Proving System (SB, BH, DH, CW), pp. 672–674.
CADECADE-1986-ButlerLMO #automation #proving #theorem proving
Paths to High-Performance Automated Theorem Proving (RB, ELL, WM, RAO), pp. 588–597.
CADECADE-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.
CADECADE-1986-GnaedigL #commutative #proving #term rewriting #termination
Proving Termination of Associative Commutative Rewriting Systems by Rewriting (IG, PL), pp. 52–61.
CADECADE-1986-HsiangR #proving #theorem proving
A New Method for Establishing Refutational Completeness in Theorem Proving (JH, MR), pp. 141–152.
CADECADE-1986-Huet86a #proving #theorem proving
Theorem Proving Systems of the Formel Project (GPH), pp. 687–688.
CADECADE-1986-LoganantharajM #graph #parallel #proving #theorem proving
Parallel Theorem Proving with Connection Graphs (RL, RAM), pp. 337–352.
CADECADE-1986-ThistlewaiteMM #automation #proving #theorem proving
The KRIPKE Automated Theorem Proving System (PBT, MAM, RKM), pp. 705–706.
CADECADE-1986-Toyama #equivalence #how #induction #term rewriting
How to Prove Equivalence of Term Rewriting Systems without Induction (YT), pp. 118–127.
LICSLICS-1986-ChouK #geometry #on the #proving #theorem proving
On Mechanical Theorem Proving in Minkowskian Plane Geometry (SCC, HPK), pp. 187–192.
LICSLICS-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.
RTARTA-1985-ChoppyJ #named #petri net #proving #term rewriting
PETRIREVE: Proving Petri Net Properties with Rewriting Systems (CC, CJ), pp. 271–286.
RTARTA-1985-DetlefsF #automation #proving #set #termination
A Procedure for Automatically Proving the Termination of a Set of Rewrite Rules (DD, RF), pp. 255–270.
RTARTA-1985-Hsiang #proving #term rewriting #theorem proving
Two Results in Term Rewriting Theorem Proving (JH), pp. 301–324.
CADECADE-1984-Plaisted #analysis #dependence #graph #proving #theorem proving #using
Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving (DAP), pp. 356–374.
CADECADE-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.
ICALPICALP-1983-HsiangD #proving #theorem proving
Rewrite Methods for Clausal and Non-Clausal Theorem Proving (JH, ND), pp. 331–346.
ICALPICALP-1983-MannaP #precedence #proving
Proving Precedence Properties: The Temporal Way (ZM, AP), pp. 491–512.
POPLPOPL-1983-NagleJ #automation #embedded #proving #realtime #verification
Practical Program Verification: Automatic Program Proving for Real-Time Embedded Software (JN, SJ), pp. 48–58.
STOCSTOC-1982-PachlKR #algorithm #bound #distributed #proving
A Technique for Proving Lower Bounds for Distributed Maximum-Finding Algorithms (JKP, EK, DR), pp. 378–382.
CADECADE-1982-Wos #automation
Solving Open Questions with an Automated Theorem-Proving Program (LW), pp. 1–31.
ICLPILPC-1982-BarbutiDL82 #logic programming #proving #source code #towards
Toward an Inductionless Technique for Proving Properties of Logic Programs (RB, PD, GL), pp. 175–181.
DACDAC-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.
ICALPICALP-1981-Snir #bound #proving
Proving Lower Bounds for Linar Decision Trees (MS), pp. 305–315.
ICSEICSE-1981-RamamrithamK #process #proving #specification
Specifying and Proving Properties of Sentinel Processes (KR, RMK), pp. 374–386.
SOSPSOSP-1981-BernsteinH #logic #proving #realtime #source code
Proving Real-Time Properties of Programs with Temporal Logic (AJB, PKHJ), pp. 1–11.
ICALPICALP-1980-Turchin #optimisation #proving #theorem proving
The Use of Metasystem Transition in Theorem Proving and Program Optimization (VFT), pp. 645–657.
POPLPOPL-1980-Musser #data type #induction #on the #proving
On Proving Inductive Properties of Abstract Data Types (DRM), pp. 154–162.
CCSDCG-1980-ThatcherWW #compilation #proving
More on advice on structuring compilers and proving them correct (JWT, EGW, JBW), pp. 165–188.
CADECADE-1980-Guguen #algebra #how #induction
How to Prove Algebraic Inductive Hypotheses Without Induction (JAG), pp. 356–373.
CADECADE-1980-Kott #proving #recursion #source code
A System for Proving Equivalences of Recursive Programs (LK), pp. 63–69.
CADECADE-1980-Nederpelt #approach #proving #theorem proving #λ-calculus
An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus (RN), pp. 182–194.
CADECADE-1980-OverbeekL #architecture #data type #implementation #source code
Data Structures and Control Architectures for Implementation of Theorem-Proving Programs (RAO, ELL), pp. 232–249.
CADECADE-1980-Plaisted #abstraction #proving #theorem proving
Abstraction Mappings in Mechanical Theorem Proving (DAP), pp. 264–280.
VLDBVLDB-1979-GardarinM #consistency #database #proving #transaction
Proving Consistency of Database Transactions (GG, MAM), pp. 291–298.
ICALPICALP-1979-DershowitzM #multi #order #proving #termination
Proving termination with Multiset Orderings (ND, ZM), pp. 188–202.
ICALPICALP-1979-DuncanY #algorithm #correctness #proving
Studies in Abstract/Concrete Mappings in Proving Algorithm Correctness (AGD, LY), pp. 218–229.
ICALPICALP-1979-ThatcherWW #compilation #proving
More on Advice on Structuring Compilers and Proving Them Correct (JWT, EGW, JBW), pp. 596–615.
POPLPOPL-1979-GoodC #proving #source code
Principles of Proving Programs Correct in Gypsy (DIG, RMC, JKW), pp. 42–52.
STOCSTOC-1977-HarelPS #axiom #deduction #proving #recursion #source code
A Complete Axiomatic System for Proving Deductions about Recursive Programs (DH, AP, JS), pp. 249–260.
SOSPSOSP-1977-FeiertagLR #design #multi #proving #security
Proving Multilevel Security of a System Design (RJF, KNL, LR), pp. 57–65.
ICALPICALP-1976-Brand #proving #source code
Proving Programs Incorrect (DB), pp. 201–227.
ICALPICALP-1976-Galil #integer #on the #programming #proving #theorem proving
On Enumeration Procedures for Theorem Proving and for Integer Programming (ZG), pp. 355–381.
ICALPICALP-1976-Schwarz #proving #reasoning #source code #termination
Event Based Reasoning — A System for Proving Correct Termination of Programs (JS), pp. 131–146.
POPLPOPL-1976-Geller #correctness #proving #testing
Test Data as an Aid in Proving Program Correctness (MMG), pp. 209–218.
ICSEICSE-1976-MannaW #correctness #proving
Is “Sometime” Sometimes Better Than “Always”? Intermittent Assertions in Proving Program Correctness (ZM, RJW), pp. 32–39.
SOSPSOSP-J-1975-Howard76 #monitoring #proving
Proving Monitors (JHH), pp. 273–279.
STOCSTOC-1975-OppenC #data type #proving #source code
Proving Assertions about Programs that Manipulate Data Structures (DCO, SAC), pp. 107–116.
POPLPOPL-1975-Lipton #named #process #proving #reduction
Reduction: A New Method of Proving Properties of Systems of Processes (RJL), pp. 78–86.
STOCSTOC-1973-Wand
An Unusual Application of Program-Proving (MW), pp. 59–66.
POPLPOPL-1973-Morris73a #compilation #proving
Advice on Structuring Compilers and Proving Them Correct (FLM), pp. 144–152.
SIGMODSIGFIDET-1972-HawryszkiewyczD #approach #correctness #database #proving
An Approach to Proving the Correctness of Data Base Operations (IH, JBD), pp. 323–348.
STOCSTOC-1971-Cook #complexity
The Complexity of Theorem-Proving Procedures (SAC), pp. 151–158.
STOCSTOC-1970-Reiter #proving #theorem 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.