BibSLEIGH — proof stem

Used together with:

system (117)
program (116)
logic (95)
base (55)
abstract (48)

Stem proof$ (all stems)

896 papers:

DATE-2015-ReichPEB #component #design #flexibility #proving: Silicon proof of the intelligent analog IP design flow for flexible automotive components (TR, HDBP, UE, RB), pp. 403–404.
DRR-2015-LamiroyBBCGHL #concept #documentation #parametricity: Re-typograph phase I: a proof-of-concept for typeface parameter extraction from historical documents (BL, TB, JB, HC, SG, RH, ML).
VLDB-2015-PapadopoulosPTT #authentication #pattern matching #proving: Practical Authenticated Pattern Matching with Optimal Proof Size (DP, CP, RT, NT), pp. 750–761.
TACAS-2015-CiniF #ltl #proving #runtime #verification: An LTL Proof System for Runtime Verification (CC, AF), pp. 581–595.
TACAS-2015-MolnarDVB #incremental #induction #ltl #model checking #proving: Saturation-Based Incremental LTL Model Checking with Inductive Proofs (VM, DD, AV, TB), pp. 643–657.
TACAS-2015-TschannenFNP #functional #named #object-oriented #source code #verification: AutoProof: Auto-Active Functional Verification of Object-Oriented Programs (JT, CAF, MN, NP), pp. 566–580.
PLDI-2015-ChuJT #automation #imperative #induction #proving #source code: Automatic induction proofs of data-structures in imperative programs (DHC, JJ, MTT), pp. 457–466.
STOC-2015-DingSS #proving #satisfiability #scalability: Proof of the Satisfiability Conjecture for Large k (JD, AS, NS), pp. 59–68.
ICALP-v1-2015-CoudronV #approximate #interactive #proving: Interactive Proofs with Approximately Commuting Provers (MC, TV), pp. 355–366.
ICALP-v1-2015-GoldreichGR #branch #context-free grammar #proving #proximity #source code: Proofs of Proximity for Context-Free Languages and Read-Once Branching Programs — (Extended Abstract) (OG, TG, RDR), pp. 666–677.
ICALP-v2-2015-AisenbergBBCI #principle #proving: Short Proofs of the Kneser-Lovász Coloring Principle (JA, MLB, SB, AC, GI), pp. 44–55.
SEFM-2015-KringsBL #proving: From Failure to Proof: The ProB Disprover for B and Event-B (SK, JB, ML), pp. 199–214.
ICFP-2015-Blanchette0T #perspective #proving #recursion: Foundational extensible corecursion: a proof assistant perspective (JCB, AP, DT), pp. 192–204.
KDD-2015-Pratt #machine learning #predict #protocol #proving: Proof Protocol for a Machine Learning Technique Making Longitudinal Predictions in Dynamic Contexts (KBP), pp. 2049–2058.
Onward-2015-GreweEWM #performance #proving #type system: Type systems for the masses: deriving soundness proofs and efficient checkers (SG, SE, PW, MM), pp. 137–150.
PPDP-2015-Miller #logic programming #proving: Proof checking and logic programming (DM), p. 18.
POPL-2015-DelawarePGC #data type #deduction #named #proving #synthesis: Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant (BD, CPC, JG, AC), pp. 689–700.
POPL-2015-FarzanKP #bound #parallel #proving: Proof Spaces for Unbounded Parallelism (AF, ZK, AP), pp. 407–420.
SAC-2015-JakobsW #analysis #data flow #proving #source code: Programs from proofs of predicated dataflow analyses (MCJ, HW), pp. 1729–1736.
ICSE-v2-2015-EtienneMAD #modelling #performance #predict #process #proving #trust: Improving Predictability, Efficiency and Trust of Model-Based Proof Activity (JFÉ, MM, FA, VD), pp. 139–148.
SPLC-2015-McGeeM #architecture #composition #cyber-physical: Composition of proof-carrying architectures for cyber-physical systems (ETM, JDM), pp. 419–426.
CADE-2015-GorznyP #first-order #proving #towards: Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses (JG, BWP), pp. 356–366.
CADE-2015-GransdenWR #automaton #named #proving #using: SEPIA: Search for Proofs Using Inferred Automata (TG, NW, RR), pp. 246–255.
CADE-2015-HeuleHW #proving #symmetry: Expressing Symmetry Breaking in DRAT Proofs (MH, WAHJ, NW), pp. 591–606.
CADE-2015-KissingerZ #diagrams #named #proving #reasoning: Quantomatic: A Proof Assistant for Diagrammatic Reasoning (AK, VZ), pp. 326–336.
CADE-2015-PientkaC #induction #programming #proving: Inductive Beluga: Programming Proofs (BP, AC), pp. 272–281.
CADE-2015-RegerTV #proving: Cooperating Proof Attempts (GR, DT, AV), pp. 339–355.
CAV-2015-ZhuPJ #named #proving #smt: Poling: SMT Aided Linearizability Proofs (HZ, GP, SJ), pp. 3–19.
CSL-2015-SchubertDB #automaton #proving: Automata Theoretic Account of Proof Search (AS, WD, HPB), pp. 128–143.
ISSTA-2015-AquinoBCDP #constraints #program analysis #proving #reuse: Reusing constraint proofs in program analysis (AA, FAB, MC, GD, MP), pp. 305–315.
LICS-2015-BaazLR #complexity #proving: A Note on the Complexity of Classical and Intuitionistic Proofs (MB, AL, GR), pp. 657–666.
LICS-2015-HeijltjesH #bound #complexity #logic #petri net #proving: Complexity Bounds for Sum-Product Logic via Additive Proof Nets and Petri Nets (WH, DJDH), pp. 80–91.
RTA-2015-AvanziniST #certification #complexity #proving #using: Certification of Complexity Proofs using CeTA (MA, CS, RT), pp. 23–39.
TLCA-2015-Bagnol #diagrams #equivalence #proving: MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams (MB), pp. 60–75.
TLCA-2015-WangC #independence #type system: A Proof-theoretic Characterization of Independence in Type Theory (YW, KC), pp. 332–346.
VMCAI-2015-GhorbalSP #algebra #difference #proving #set: A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets (KG, AS, AP), pp. 431–448.
DATE-2014-Jin #evaluation #proving #security #tool support #trust: EDA tools trust evaluation through security property proofs (YJ), pp. 1–4.
PODS-2014-BenediktCT #generative #low cost #proving: Generating low-cost plans from proofs (MB, BtC, ET), pp. 200–211.
VLDB-2014-BenediktLT #named #query: PDQ: Proof-driven Query Answering over Web-based Data (MB, JL, ET), pp. 1553–1556.
ESOP-2014-BrainDKS #generative #proving #source code: Model and Proof Generation for Heap-Manipulating Programs (MB, CD, DK, PS), pp. 432–452.
ESOP-2014-YoshimizuHFL #higher-order #metric #proving #quantum: Measurements in Proof Nets as Higher-Order Quantum Circuits (AY, IH, CF, UDL), pp. 371–391.
PLDI-2014-PekQM #c #data type #logic #proving #using: Natural proofs for data structure manipulation in C using separation logic (EP, XQ, PM), p. 46.
PLDI-2014-RickettsRJTL #automation #proving: Automating formal proofs for reactive systems (DR, VR, DJ, ZT, SL), p. 47.
STOC-2014-KalaiRR #how #power of #proving: How to delegate computations: the power of no-signaling proofs (YTK, RR, RDR), pp. 485–494.
AFL-2014-Valmari #proving #string: Character Strings and Gödel’s Incompleteness Proof (AV), pp. 355–369.
ICALP-v1-2014-Ben-SassonRTW #algorithm #proving: Sampling-Based Proofs of Almost-Periodicity Results and Algorithmic Applications (EBS, NRZ, MT, JW), pp. 955–966.
ICALP-v1-2014-OstrovskyPV #on the #proving: On Input Indistinguishable Proof Systems (RO, GP, IV), pp. 895–906.
ICALP-v1-2014-TalwarW #proving: Balanced Allocations: A Simple Proof for the Heavily Loaded Case (KT, UW), pp. 979–990.
FM-2014-FreitasW #formal method #proving: Proof Patterns for Formal Methods (LF, IW), pp. 279–295.
FM-2014-Klein #proving: Proof Engineering Considered Essential (GK), pp. 16–21.
FM-2014-LeinoM #automation #induction #proving #verification: Co-induction Simply — Automatic Co-inductive Proofs in a Program Verifier (KRML, MM), pp. 382–398.
IFM-2014-ErikssonPB #invariant #programming #proving: Proofs and Refutations in Invariant-Based Programming (JE, MP, RJB), pp. 189–204.
IFM-2014-TofanSR #composition #multi #proving: A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset (BT, GS, WR), pp. 357–372.
SEFM-2014-Leroy #code generation #proving #tool support #verification: Formal Proofs of Code Generation and Verification Tools (XL), pp. 1–4.
HCI-AIMT-2014-RederMFK #arduino #concept #human-computer #interactive #interface #proving: Neural Interface Emotiv EPOC and Arduino: Brain-Computer Interaction in a Proof of Concept (EER, ARdQM, VRTF, FK), pp. 612–623.
LCT-NLE-2014-PaisT #deduction #first-order #logic #novel #proving: Novel Didactic Proof Assistant for First-Order Logic Natural Deduction (JP, AT), pp. 441–451.
OOPSLA-2014-Desai0M #proving #reduction #source code #using: Natural proofs for asynchronous programs using almost-synchronous reductions (AD, PG, PM), pp. 709–725.
PPDP-2014-Ilik #continuation #normalisation #proving #tutorial: Proofs in continuation-passing style: normalization of Gödel’s System T extended with sums and delimited control operators: Distilled Tutorial (DI), pp. 55–56.
POPL-2014-Benton0N #logic: Abstract effects and proof-relevant logical relations (NB, MH, VN), pp. 619–632.
POPL-2014-CasinghinoSW #proving #source code: Combining proofs and programs in a dependently typed language (CC, VS, SW), pp. 33–46.
POPL-2014-ChaudhuriCS #proving #synthesis #using: Bridging boolean and quantitative synthesis using smoothed proof search (SC, MC, ASL), pp. 207–220.
POPL-2014-FarzanKP #proving: Proofs that count (AF, ZK, AP), pp. 151–164.
POPL-2014-HouCGT #logic #proving: Proof search for propositional abstract separation logics via labelled sequents (ZH, RC, RG, AT), pp. 465–476.
POPL-2014-LeeP #logic #proving: A proof system for separation logic with magic wand (WL, SP), pp. 477–490.
ICLP-J-2014-PimentelON #concurrent #constraints #programming #proving: A Proof Theoretic Study of Soft Concurrent Constraint Programming (EP, CO, VN), pp. 649–663.
IJCAR-2014-BeesonW #geometry #proving: OTTER Proofs in Tarskian Geometry (MB, LW), pp. 495–510.
IJCAR-2014-BoudouFP #named #proving: Skeptik: A Proof Compression System (JB, AF, BWP), pp. 374–380.
IJCAR-2014-HeuleSB #preprocessor #proving: A Unified Proof System for QBF Preprocessing (MH, MS, AB), pp. 91–106.
ISSTA-2014-Chen #constraints #program analysis #proving #reuse #scalability: Reusing constraint proofs for scalable program analysis (MC), pp. 449–452.
LICS-CSL-2014-Ehrhard #correctness #proving: A new correctness criterion for MLL proof nets (TE), p. 10.
LICS-CSL-2014-HeijltjesH #equivalence #proving: No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete (WH, RH), p. 10.
LICS-CSL-2014-Mahboubi #order #proving #theorem: Computer-checked mathematics: a formal proof of the odd order theorem (AM), p. 1.
RTA-TLCA-2014-Czajka #confluence #induction #proving #λ-calculus: A Coinductive Confluence Proof for Infinitary λ-Calculus (LC), pp. 164–178.
RTA-TLCA-2014-LombardiRV #proving: Proof Terms for Infinitary Rewriting (CL, AR, RdV), pp. 303–318.
RTA-TLCA-2014-Maieli #proving: Construction of Retractile Proof Structures (RM), pp. 319–333.
RTA-TLCA-2014-SternagelT #algebra #certification #complexity #formal method #proving #termination: Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs (CS, RT), pp. 441–455.
SAT-2014-BalabanovWJ #proving: QBF Resolution Systems and Their Proof Complexities (VB, MW, JHRJ), pp. 154–169.
SAT-2014-BelovHM #proving #using: MUS Extraction Using Clausal Proofs (AB, MH, JMS), pp. 48–57.
SAT-2014-IstrateC #complexity #proving #theorem: Proof Complexity and the Kneser-Lovász Theorem (GI, AC), pp. 138–153.
SAT-2014-MiksaN #proving: Long Proofs of (Seemingly) Simple Formulas (MM, JN), pp. 121–137.
SAT-2014-Nordstrom #bibliography #complexity #proving #satisfiability: A (Biased) Proof Complexity Survey for SAT Practitioners (JN), pp. 1–6.
SAT-2014-WetzlerHH #named #performance #proving #using: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (NW, MH, WAHJ), pp. 422–429.
TAP-2014-KosmatovLA #case study #proving #testing #verification: A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing (NK, ML, CA), pp. 158–164.
ESOP-2013-WickersonDP #logic #proving: Ribbon Proofs for Separation Logic (JW, MD, MJP), pp. 189–208.
FoSSaCS-2013-MioS #composition #concurrent #probability #process #proving #verification: A Proof System for Compositional Verification of Probabilistic Concurrent Processes (MM, AS), pp. 161–176.
TACAS-2013-ChristHN #proving: Proof Tree Preserving Interpolation (JC, JH, AN), pp. 124–138.
TACAS-2013-LiDDMS #abduction #composition #proving #synthesis: Synthesis of Circular Compositional Program Proofs via Abduction (BL, ID, TD, KLM, MS), pp. 370–384.
PLDI-2013-Qiu0SM #proving: Natural proofs for structure, data, and separation (XQ, PG, AS, PM), pp. 231–242.
STOC-2013-Ben-SassonCGT #on the #performance #proving: On the concrete efficiency of probabilistically-checkable proofs (EBS, AC, DG, ET), pp. 585–594.
STOC-2013-BitanskyCCT #composition #recursion: Recursive composition and bootstrapping for SNARKS and proof-carrying data (NB, RC, AC, ET), pp. 111–120.
STOC-2013-RothblumVW #interactive #proving #proximity #sublinear: Interactive proofs of proximity: delegating computation in sublinear time (GNR, SPV, AW), pp. 793–802.
STOC-2013-Williams #proving: Natural proofs versus derandomization (RW), pp. 21–30.
DLT-2013-Regnault #automaton #probability #proving: Proof of a Phase Transition in Probabilistic Cellular Automata (DR), pp. 433–444.
ICALP-v2-2013-BecchettiBDKM #bound #complexity #convergence #proving: Physarum Can Compute Shortest Paths: Convergence Proofs and Complexity Bounds (LB, VB, MD, AK, KM), pp. 472–483.
ICALP-v2-2013-Stirling #proving #λ-calculus: Proof Systems for Retracts in Simply Typed λ Calculus (CS), pp. 398–409.
LATA-2013-RotBR #equivalence #induction #proving: Coinductive Proof Techniques for Language Equivalence (JR, MMB, JJMMR), pp. 480–492.
IFM-2013-Abrial #proving #source code: From Z to B and then Event-B: Assigning Proofs to Meaningful Programs (JRA), pp. 1–15.
KEOD-2013-AkamaN #problem #proving: Embedding Proof Problems into Query-answering Problems and Problem Solving by Equivalent Transformation (KA, EN), pp. 253–260.
SEKE-2013-Alegroth #concept #proving #random #testing #user interface #visual notation: Random Visual GUI Testing: Proof of Concept (EA), pp. 178–183.
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.
POPL-2013-Gonthier #order #proving #theorem: Engineering mathematics: the odd order theorem proof (GG), pp. 1–2.
POPL-2013-HurNDV #induction #power of #proving: The power of parameterization in coinductive proof (CKH, GN, DD, VV), pp. 193–206.
ESEC-FSE-2013-Nori0 #proving #termination #testing: Termination proofs from tests (AVN, RS), pp. 246–256.
CADE-2013-ChihaniMR #first-order #logic #proving: Foundational Proof Certificates in First-Order Logic (ZC, DM, FR), pp. 162–177.
CADE-2013-ClaessenJRS #automation #induction #proving #using: Automating Inductive Proofs Using Theory Exploration (KC, MJ, DR, NS), pp. 392–406.
CADE-2013-KaliszykU #named #proving #re-engineering: PRocH: Proof Reconstruction for HOL Light (CK, JU), pp. 267–274.
CADE-2013-Mayer #hybrid #logic #proving #transitive: A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies (MCM), pp. 76–90.
CAV-2013-DragoiGH #automation #concurrent #proving: Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates (CD, AG, TAH), pp. 174–190.
CAV-2013-WonischSW #proving #source code: Programs from Proofs — A PCC Alternative (DW, AS, HW), pp. 912–927.
CSL-2013-FortierS #proving #semantics: Cuts for circular proofs: semantics and cut-elimination (JF, LS), pp. 248–262.
CSL-2013-GhasemlooC #bound #proving: Theories for Subexponential-size Bounded-depth Frege Proofs (KG, SAC), pp. 296–315.
ISSTA-2013-Bonacchi #case study #proving #safety: Formal safety proof: a real case study in a railway interlocking system (AB0), pp. 378–381.
LICS-2013-Halpern #first-order #logic #proving #security #using: From Qualitative to Quantitative Proofs of Security Properties Using First-Order Conditional Logic (JYH), pp. 2–3.
RTA-2013-FelgenhauerO #diagrams #order #proving: Proof Orders for Decreasing Diagrams (BF, VvO), pp. 174–189.
SAT-2013-Atserias #algebra #bound #problem #proving: The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-algebraic Proofs (AA), pp. 1–17.
SAT-2013-Johannsen #exponential #learning #proving: Exponential Separations in a Hierarchy of Clause Learning Proof Systems (JJ), pp. 40–51.
SAT-2013-Lauria #bound #proving #rank #theorem: A Rank Lower Bound for Cutting Planes Proofs of Ramsey’s Theorem (ML), pp. 351–364.
TAP-2013-KosmatovPS #proving #source code #tutorial: A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper (NK, VP, JS), pp. 168–177.
TLCA-2013-BentonHN #generative #logic: Proof-Relevant Logical Relations for Name Generation (NB, MH, VN), pp. 48–60.
VMCAI-2013-Podelski #automaton #proving: Automata as Proofs (AP), pp. 13–14.
CASE-2012-LakshmiNBSSBV #reduction: A strategy-proof and budget balanced mechanism for carbon footprint reduction by global companies (LUL, YN, DB, PS, SVS, SB, NV), pp. 64–69.
TACAS-2012-PopeeaR #composition #concurrent #multi #proving #source code #termination #thread: Compositional Termination Proofs for Multi-threaded Programs (CP, AR), pp. 237–251.
TACAS-2012-UlbrichGGT #alloy #proving #specification: A Proof Assistant for Alloy Specifications (MU, UG, AAEG, MT), pp. 422–436.
PLDI-2012-GrebenshchikovLPR #proving #verification: Synthesizing software verifiers from proof rules (SG, NPL, CP, AR), pp. 405–416.
SAS-2012-BartheGB #encryption #proving: Computer-Aided Cryptographic Proofs (GB, BG, SZB), pp. 1–2.
SAS-2012-ChenFM #linear #proving #termination: Termination Proofs for Linear Simple Loops (HYC, SF, SM), pp. 422–438.
SAS-2012-Midtgaard0M #proving: A Structural Soundness Proof for Shivers’s Escape Technique — A Case for Galois Connections (JM, MDA, MM), pp. 352–369.
STOC-2012-AzarM #proving: Rational proofs (PDA, SM), pp. 1017–1028.
STOC-2012-BarakBHKSZ #proving: Hypercontractivity, sum-of-squares proofs, and their applications (BB, FGSLB, AWH, JAK, DS, YZ), pp. 307–326.
STOC-2012-HrubesT #proving: Short proofs for the determinant identities (PH, IT), pp. 193–212.
STOC-2012-HuynhN #communication #complexity #on the #proving #trade-off: On the virtue of succinct proofs: amplifying communication complexity hardness to time-space trade-offs in proof complexity (TH, JN), pp. 233–248.
LATA-2012-Hetzl #proving: Applying Tree Languages in Proof Theory (SH), pp. 301–312.
FM-2012-CousineauDLMRV #proving: TLA + Proofs (DC, DD, LL, SM, DR, HV), pp. 147–154.
IFM-2012-LensinkSE #concurrent #framework #proving #source code: A Proof Framework for Concurrent Programs (LL, SS, MCJDvE), pp. 174–190.
SEFM-2012-MatichukM #automation #proving #specification: Extensible Specifications for Automatic Re-use of Specifications and Proofs (DM, TCM), pp. 333–341.
ICFP-2012-MyreenO #higher-order #logic #ml #synthesis: Proof-producing synthesis of ML from higher-order logic (MOM, SO), pp. 115–126.
ICFP-2012-VytiniotisJM #compilation #fault #proving #similarity: Equality proofs and deferred type errors: a compiler pearl (DV, SLPJ, JPM), pp. 341–352.
IFL-2012-WaltS #proving: Engineering Proof by Reflection in Agda (PvdW, WS), pp. 157–173.
CHI-2012-LazarFBMWHOE #approach #interactive #proving: The SoundsRight CAPTCHA: an improved approach to audio human interaction proofs for blind users (JL, JF, TB, GM, BW, JH, AO, NE), pp. 2267–2276.
KR-2012-TosattoBTV #proving #semantics: Abstract Normative Systems: Semantics and Proof Theory (SCT, GB, LWNvdT, SV).
POPL-2012-HoderKV #game studies #proving: Playing in the grey area of proofs (KH, LK, AV), pp. 259–272.
POPL-2012-MadhusudanQS #induction #proving #recursion: Recursive proofs for inductive tree data-structures (PM, XQ, AS), pp. 123–136.
POPL-2012-StampoulisS #proving: Static and user-extensible proof checking (AS, ZS), pp. 273–284.
CAV-2012-BrockschmidtMOG #automation #java #proving #source code #termination: Automated Termination Proofs for Java Programs with Cyclic Data (MB, RM, CO, JG), pp. 105–122.
CSL-2012-Cook #complexity #proving: Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (Invited Talk) (SAC), pp. 9–11.
CSL-2012-Kuroda #axiom #bound #concept #proving: Axiomatizing proof tree concepts in Bounded Arithmetic (SK), pp. 440–454.
CSL-2012-Rabinovich #proving #theorem: A Proof of Kamp’s theorem (AR), pp. 516–527.
ICLP-J-2012-Cervesato #compilation #logic programming #source code: An Improved Proof-Theoretic Compilation of Logic Programs (IC), pp. 639–657.
IJCAR-2012-JacquelBDD #automation #deduction #modulo theories #proving #theorem proving #using #verification: Tableaux Modulo Theories Using Superdeduction — An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover (MJ, KB, DD, CD), pp. 332–338.
IJCAR-2012-UrbasJ #named #proving: Diabelli: A Heterogeneous Proof System (MU, MJ), pp. 559–566.
LICS-2012-Herbelin #logic #proving: A Constructive Proof of Dependent Choice, Compatible with Classical Logic (HH), pp. 365–374.
LICS-2012-Platzer12a #hybrid #proving: The Complete Proof Theory of Hybrid Systems (AP), pp. 541–550.
RTA-2012-CousineauH #proving #semantics: A Semantic Proof that Reducibility Candidates entail Cut Elimination (DC, OH), pp. 133–148.
SAT-2012-Gupta #algorithm #proving #reduction: Improved Single Pass Algorithms for Resolution Proof Reduction — (Poster Presentation) (AG), pp. 469–470.
VMCAI-2012-Nipkow #education #proving #semantics: Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs (TN), pp. 24–38.
VLDB-2012-CormodeTY11 #interactive #proving #streaming #verification: Verifying Computations with Streaming Interactive Proofs (GC, JT, KY), pp. 25–36.
STOC-2011-KawarabayashiW #algorithm #composition #graph #proving: A simpler algorithm and shorter proof for the graph minor decomposition (KiK, PW), pp. 451–458.
ICALP-v1-2011-FaustPV #how: Tamper-Proof Circuits: How to Trade Leakage for Tamper-Resilience (SF, KP, DV), pp. 391–402.
LATA-2011-Leroux #problem #proving #reachability #self: Vector Addition System Reachability Problem: A Short Self-contained Proof (JL), pp. 41–64.
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-GonthierZND #ad hoc #automation #how #proving: How to make ad hoc proof automation less ad hoc (GG, BZ, AN, DD), pp. 163–175.
MoDELS-2011-JacksonLB #automation #metamodelling #proving #reasoning #specification: Reasoning about Metamodeling with Formal Specifications and Automatic Proofs (EKJ, TL, DB), pp. 653–667.
MoDELS-2011-JacksonLB #automation #metamodelling #proving #reasoning #specification: Reasoning about Metamodeling with Formal Specifications and Automatic Proofs (EKJ, TL, DB), pp. 653–667.
LOPSTR-2011-CaballeroRVM #debugging #declarative #maude #proving: Simplifying Questions in Maude Declarative Debugger by Transforming Proof Trees (RC, AR, AV, NMO), pp. 73–89.
PPDP-2011-Guenot #proving #reduction #λ-calculus: Nested proof search as reduction in the λ-calculus (NG), pp. 183–194.
POPL-2011-Leroux #problem #proving #reachability #self: Vector addition system reachability problem: a short self-contained proof (JL), pp. 307–316.
SAC-2011-BackP #invariant #proving #semantics #source code: Semantics and proof rules of invariant based programs (RJB, VP), pp. 1658–1665.
SAC-2011-Mammar #approach #bibliography #c #detection: An overview of a proof-based approach to detecting C vulnerabilities (AM), pp. 1343–1344.
SAC-2011-MammarFD #approach #reachability #verification: A proof-based approach to verifying reachability properties (AM, MF, FD), pp. 1651–1657.
CC-2011-Odersky #parallel #persistent: Future-Proofing Collections: From Mutable to Persistent to Parallel (MO), p. 1.
PPoPP-2011-BotincanDDP #automation #memory management #proving #safety: Automatic safety proofs for asynchronous memory operations (MB, MD, AFD, MJP), pp. 313–314.
CADE-2011-BrotherstonDP #automation #logic #proving: Automated Cyclic Entailment Proofs in Separation Logic (JB, DD, RLP), pp. 131–146.
CADE-2011-FontaineMP #proving: Compression of Propositional Resolution Proofs via Partial Regularization (PF, SM, BWP), pp. 237–251.
CAV-2011-BalabanovJ #evaluation #proving: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications (VB, JHRJ), pp. 149–164.
LICS-2011-ChurchillLM #game studies #imperative #proving #semantics #source code: Imperative Programs as Proofs via Game Semantics (MC, JL, GM), pp. 65–74.
LICS-2011-Heijltjes #linear #logic #proving: Proof Nets for Additive Linear Logic with Units (WH), pp. 207–216.
LICS-2011-Pitassi #bibliography #complexity #proving #state of the art: Propositional Proof Complexity: A Survey on the State of the Art, Including Some Recent Results (TP), p. 119.
RTA-2011-BrockschmidtOG #bytecode #composition #java #proving #recursion #source code #term rewriting #termination: Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting (MB, CO, JG), pp. 155–170.
RTA-2011-ContejeanCFPU #automation #proving: Automated Certified Proofs with CiME3 (EC, PC, JF, OP, XU), pp. 21–30.
RTA-2011-MoserS #complexity #dependence #framework #multi #proving #recursion #termination: Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity (GM, AS), pp. 235–250.
RTA-2011-Weirich #proving #source code: Combining Proofs and Programs (SW), p. 9.
TAP-2011-Godefroid #proving #testing: Tests from Proofs (PG), p. 14.
TLCA-2011-Gimenez #difference #linear #logic #normalisation #proving: Realizability Proof for Normalization of Full Differential Linear Logic (SG), pp. 107–122.
TLCA-2011-Weirich #proving #source code: Combining Proofs and Programs (SW), p. 9.
VMCAI-2011-PiskacW #automation #proving #termination: Decision Procedures for Automating Termination Proofs (RP, TW), pp. 371–386.
VLDB-2010-CaoKRT #named #transaction: rho-uncertainty: Inference-Proof Transaction Anonymization (JC, PK, CR, KLT), pp. 1033–1044.
ESOP-2010-DeshmukhRRV #concurrent #logic #proving: Logical Concurrency Control from Sequential Proofs (JVD, GR, VPR, KV), pp. 226–245.
FoSSaCS-2010-CateF #calculus #finite #proving #μ-calculus: An Easy Completeness Proof for the Modal μ-Calculus on Finite Trees (BtC, GF), pp. 161–175.
TACAS-2010-ElmasQSST #abstraction #proving #reduction: Simplifying Linearizability Proofs with Reduction and Abstraction (TE, SQ, AS, OS, ST), pp. 296–311.
WRLA-2010-Shankar #proving: Rewriting, Inference, and Proof (NS), pp. 1–14.
PEPM-2010-ContejeanPUCPF #approach #automation #proving #termination: A3PAT, an approach for certified automated termination proofs (EC, AP, XU, PC, OP, JF), pp. 63–72.
SAS-2010-KatoenMMM #automation #generative #invariant #probability #source code: Linear-Invariant Generation for Probabilistic Programs: — Automated Support for Proof-Based Methods (JPK, AM, LM, CCM), pp. 390–406.
STOC-2010-BeameHP #complexity #proving: Hardness amplification in proof complexity (PB, TH, TP), pp. 87–96.
STOC-2010-KawarabayashiW #algorithm #graph #proving #theorem: A shorter proof of the graph minor algorithm: the unique linkage theorem (KiK, PW), pp. 687–694.
ICALP-v1-2010-AtseriasM #game studies #proving: Mean-Payoff Games and Propositional Proofs (AA, ENM), pp. 102–113.
ICALP-v2-2010-ChenF #logic #on the #proving: On p-Optimal Proof Systems and Logics for PTIME (YC, JF), pp. 321–332.
LATA-2010-LetichevskySS #automaton #equivalence #finite #multi #problem #proving #using: The Equivalence Problem of Deterministic Multitape Finite Automata: A New Proof of Solvability Using a Multidimensional Tape (AAL, ASS, SKS), pp. 392–402.
IFM-2010-Stratulat #induction #proving: Integrating Implicit Induction Proofs into Certified Proof Environments (SS), pp. 320–335.
ICPR-2010-SuXCWM #concept #identification: EEG-based Personal Identification: from Proof-of-Concept to A Practical System (FS, LX, AC, YW, JM), pp. 3728–3731.
KR-2010-HorridgeP #ontology #proving #towards: From Justifications Towards Proofs for Ontology Engineering (MH, BP).
LOPSTR-2010-SakuraiA #library #named #proving #user interface #visualisation: MikiBeta: A General GUI Library for Visualizing Proof Trees — System Description and Demonstration (KS, KA), pp. 84–98.
LOPSTR-2010-Seki #induction #on the #proving: On Inductive Proofs by Extended Unfold/Fold Transformation Rules (HS), pp. 117–132.
POPL-2010-TateSL #compilation #generative #optimisation #proving: Generating compiler optimizations from proofs (RT, MS, SL), pp. 389–402.
SAC-2010-Pham #geometry #proving: Similar triangles and orientation in plane elementary geometry for Coq-based proofs (TMP), pp. 1268–1269.
SAC-2010-VogelsJP #generative #performance #proving #verification: A machine-checked soundness proof for an efficient verification condition generator (FV, BJ, FP), pp. 2517–2522.
ICSE-2010-Elmas #abstraction #concurrent #named #proving #reduction #verification: QED: a proof system based on reduction and abstraction for the static verification of concurrent software (TE), pp. 507–508.
CAV-2010-ThakurLLBDEAR #generative #proving: Directed Proof Generation for Machine Code (AVT, JL, AL, AB, ED, ME, TA, TWR), pp. 288–305.
CSL-2010-ChenF #on the #problem #proving #slicing: On Slicewise Monotone Parameterized Problems and Optimal Proof Systems for TAUT (YC, JF), pp. 200–214.
CSL-2010-Krajicek #proving: From Feasible Proofs to Feasible Computations (JK), pp. 22–31.
CSL-2010-Pous #algebra #linear #logic #proving: Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic (DP), pp. 484–498.
CSL-2010-SternagelT #dependence #proving #termination: Signature Extensions Preserve Termination — An Alternative Proof via Dependency Pairs (CS, RT), pp. 514–528.
ICLP-2010-AlbertiGL10 #abduction #constraints #proving #runtime: Runtime Addition of Integrity Constraints in an Abductive Proof Procedure (MA, MG, EL), pp. 4–13.
ICLP-2010-Guenot10 #calculus #linear #logic #proving: Focused Proof Search for Linear Logic in the Calculus of Structures (NG), pp. 84–93.
IJCAR-2010-ChaudhuriDLM #proving #safety #verification: Verifying Safety Properties with the TLA+ Proof System (KC, DD, LL, SM), pp. 142–148.
IJCAR-2010-DunchevLLWP #proving: System Description: The Proof Transformation System CERES (TD, AL, TL, DW, BWP), pp. 427–433.
RTA-2010-Aoto #automation #confluence #diagrams #proving: Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling (TA), pp. 7–16.
RTA-2010-GuglielmiGP #calculus #proving: A Proof Calculus Which Reduces Syntactic Bureaucracy (AG, TG, MP), pp. 135–150.
SAT-2010-BeyersdorffMMTV #complexity #logic #proving: Proof Complexity of Propositional Default Logic (OB, AM, SM, MT, HV), pp. 30–43.
SAT-2010-Cotton #proving: Two Techniques for Minimizing Resolution Proofs (SC), pp. 306–312.
TAP-2010-BousquetL #analysis #evaluation #mutation testing #process #proving: Proof Process Evaluation with Mutation Analysis (LdB, ML), pp. 55–60.
TAP-2010-Ernst #feedback #how #proving #testing: How Tests and Proofs Impede One Another: The Need for Always-On Static and Dynamic Feedback (MDE), pp. 1–2.
TAP-2010-GoldbergM #encoding #generative #proving #testing: Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding (EG, PM), pp. 101–116.
DATE-2009-GarciaO #embedded #fault #information management #self: Making DNA self-assembly error-proof: Attaining small growth error rates through embedded information redundancy (SG, AO), pp. 898–901.
ITiCSE-2009-Blaheta09a #array #proving #visual notation: A visual proof of amortised-linear resizable arrays (DB), p. 338.
WRLA-2008-AndreiL09 #calculus #proving: Strategy-Based Proof Calculus for Membrane Systems (OA, DL), pp. 23–43.
WRLA-2008-HolenJW09 #calculus #first-order #maude #proving: Proof Search for the First-Order Connection Calculus in Maude (BH, EBJ, AW), pp. 173–188.
TACAS-2009-GuptaMR #proving #testing: From Tests to Proofs (AG, RM, AR), pp. 262–276.
PLDI-2009-ZeeKR #imperative #proving #source code: An integrated proof language for imperative programs (KZ, VK, MCR), pp. 338–351.
SAS-2009-Hurlin #automation #optimisation #parallel #proving #source code: Automatic Parallelization and Optimization of Programs by Proof Rewriting (CH), pp. 52–68.
STOC-2009-Moser #proving: A constructive proof of the Lovász local lemma (RAM), pp. 343–350.
CIAA-2009-IosifR #proving #termination: Automata-Based Termination Proofs (RI, AR), pp. 165–177.
LATA-2009-BeyersdorffKM #complexity #nondeterminism #proving: Nondeterministic Instance Complexity and Proof Systems with Advice (OB, JK, SM), pp. 164–175.
CEFP-2009-Devai #haskell #proving: Embedding a Proof System in Haskell (GD), pp. 354–371.
ICFP-2009-ChlipalaMMSW #effectiveness #higher-order #imperative #interactive #proving #source code: Effective interactive proofs for higher-order imperative programs (AC, JGM, GM, AS, RW), pp. 79–90.
ICFP-2009-Pierce #education #programming language #proving #using: λ, the ultimate TA: using a proof assistant to teach programming language foundations (BCP), pp. 121–122.
LOPSTR-2009-Seki #induction #on the #proving: On Inductive and Coinductive Proofs via Unfold/Fold Transformations (HS), pp. 82–96.
PPDP-2009-BiernackaB #proving #termination: Context-based proofs of termination for typed delimited-control operators (MB, DB), pp. 289–300.
POPL-2009-BartheGB #certification #encryption #proving: Formal certification of code-based cryptographic proofs (GB, BG, SZB), pp. 90–101.
CC-2009-MyreenSG #compilation: Extensible Proof-Producing Compilation (MOM, KS, MJCG), pp. 2–16.
CADE-2009-Rinard #proving #reasoning: Integrated Reasoning and Proof Choice Point Selection in the Jahob System — Mechanisms for Program Survival (MCR), pp. 1–16.
CAV-2009-AbadiBC #modelling #protocol #proving #security: Models and Proofs of Protocol Security: A Progress Report (MA, BB, HCL), pp. 35–49.
CAV-2009-DilligDA #integer #linear #proving: Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers (ID, TD, AA), pp. 233–247.
CAV-2009-FuhrmannH #bound #induction #on the #proving: On Extending Bounded Proofs to Inductive Proofs (OF, SH), pp. 278–290.
CSL-2009-Berger #induction #proving: From Coinductive Proofs to Exact Real Arithmetic (UB), pp. 132–146.
CSL-2009-CiabattoniST #proving: Expanding the Realm of Systematic Proof Theory (AC, LS, KT), pp. 163–178.
ICLP-2009-PilozziS09a #automation #proving #termination: Automating Termination Proofs for CHR (PP, DDS), pp. 504–508.
LICS-2009-LiangM #calculus #proving: A Unified Sequent Calculus for Focused Proofs (CL, DM), pp. 355–364.
RTA-2009-TiuG #analysis #proving: A Proof Theoretic Analysis of Intruder Theories (AT, RG), pp. 103–117.
SAT-2009-Gelder #proving: Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces (AVG), pp. 141–146.
TLCA-2009-AbelCP #algorithm #composition #proving #type system: A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (AA, TC, MP), pp. 5–19.
TLCA-2009-LovasP #proving #refinement: Refinement Types as Proof Irrelevance (WL, FP), pp. 157–171.
TLCA-2009-Strassburger #higher-order #linear #logic #multi #proving: Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic (LS), pp. 309–324.
VMCAI-2009-AmjadB #analysis #automation #proving #towards: Towards Automatic Stability Analysis for Rely-Guarantee Proofs (HA, RB), pp. 14–28.
ASE-2008-HartKGCL #abstraction #proving #refinement: Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates (TEH, KK, AG, MC, DL), pp. 387–390.
ASE-2008-HartKGCL08a #model checking #named #proving: PtYasm: Software Model Checking with Proof Templates (TEH, KK, AG, MC, DL), pp. 479–480.
FASE-2008-BruckerW #higher-order #named #ocl #proving #uml: HOL-OCL: A Formal Proof Environment for UML/OCL (ADB, BW), pp. 97–100.
TACAS-2008-Moskal #proving #smt: Rocket-Fast Proof Checking for SMT Solvers (MM), pp. 486–500.
PEPM-2008-SaabasU #optimisation #proving: Proof optimization for partial redundancy elimination (AS, TU), pp. 91–101.
STOC-2008-GoldwasserKR #interactive #proving: Delegating computation: interactive proofs for muggles (SG, YTK, GNR), pp. 113–122.
STOC-2008-ShaltielV #proving: Hardness amplification proofs require majority (RS, EV), pp. 589–598.
FLOPS-2008-AbelCD #algebra #on the #proving #type system: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (AA, TC, PD), pp. 3–13.
ICALP-A-2008-Yin #complexity #nondeterminism #proving: Cell-Probe Proofs and Nondeterministic Cell-Probe Complexity (YY), pp. 72–83.
FM-2008-McIverMG #probability #proving #refinement: Proofs and Refutations for Probabilistic Refinement (AKM, CCM, CG), pp. 100–115.
SEFM-2008-BalakrishnanG #fault #named: PED: Proof-Guided Error Diagnosis by Triangulation of Program Error Causes (GB, MKG), pp. 268–278.
SEFM-2008-BartheKPS #hybrid #proving #verification: Preservation of Proof Pbligations for Hybrid Verification Methods (GB, CK, DP, JSF), pp. 127–136.
IFL-2008-Hinze #proving #theorem: Scans and Convolutions — A Calculational Proof of Moessner’s Theorem (RH), pp. 1–24.
KR-2008-RenzL #automation #calculus #complexity #proving: Automated Complexity Proofs for Qualitative Spatial and Temporal Calculi (JR, JJL), pp. 715–723.
ECMDA-FA-2008-MohagheghiD #bibliography #case study #experience #industrial #proving: Where Is the Proof? — A Review of Experiences from Applying MDE in Industry (PM, VD), pp. 432–443.
ICMT-2008-Poernomo: Proofs-as-Model-Transformations (IP), pp. 214–228.
TOOLS-EUROPE-2008-NordioMM #compilation #eiffel #source code: Proof-Transforming Compilation of Eiffel Programs (MN, PM, BM), pp. 316–335.
PPDP-2008-MontenegroPS #correctness #memory management #proving #type system: A type system for safe memory management and its proof of correctness (MM, RP, CS), pp. 152–162.
PPDP-2008-PientkaD #programming #proving: Programming with proofs and explicit contexts (BP, JD), pp. 163–173.
PPDP-2008-SilvaO #functional #prototype #proving #quote: “Galculator”: functional prototype of a Galois-connection based proof assistant (PFS, JNO), pp. 44–55.
POPL-2008-BrotherstonBC #logic #proving #termination: Cyclic proofs of program termination in separation logic (JB, RB, CC), pp. 101–112.
SAC-2008-Michelucci #geometry #proving #theorem #word: Isometry group, words and proofs of geometric theorems (DM), pp. 1821–1825.
SMT-2007-BongioKLLM08 #encoding #first-order #proving #smt: Encoding First Order Proofs in SMT (JB, CK, HL, CL, REM), pp. 71–84.
CAV-2008-CohenN #concurrent #linear #proving #source code: Local Proofs for Linear-Time Properties of Concurrent Programs (AC, KSN), pp. 149–161.
CSL-2008-Thomas #decidability #model transformation #monad #proving: Model Transformations in Decidability Proofs for Monadic Theories (WT), pp. 23–31.
ICLP-2008-MarekR #on the: On the Continuity of Gelfond-Lifschitz Operator and Other Applications of Proof-Theory in ASP (VWM, JBR), pp. 223–237.
ICLP-2008-Saurin #interactive #programming #proving #towards: Towards Ludics Programming: Interactive Proof Search (AS), pp. 253–268.
IJCAR-2008-BartheGP #java #proving #virtual machine: Preservation of Proof Obligations from Java to the Java Virtual Machine (GB, BG, MP), pp. 83–99.
IJCAR-2008-PerezV #effectiveness #logic #proving: Proof Systems for Effectively Propositional Logic (JANP, AV), pp. 426–440.
ISSTA-2008-BeckmanNRS #proving #testing: Proofs from tests (NEB, AVN, SKR, RJS), pp. 3–14.
LICS-2008-DelandeM #approach #proving: A Neutral Approach to Proof and Refutation in MALL (OD, DM), pp. 498–508.
LICS-2008-LaurentM #proving: Cut Elimination for Monomial MALL Proof Nets (OL, RM), pp. 486–497.
LICS-2008-NauroisM #correctness #multi #proving: Correctness of Multiplicative Additive Proof Structures is NL-Complete (PJdN, VM), pp. 476–485.
LICS-2008-Riis #calculus #complexity #on the #polynomial #proving: On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity (SR), pp. 272–283.
MBT-2008-BruckerBW #empirical #proving #verification: Verifying Test-Hypotheses: An Experiment in Test and Proof (ADB, LB, BW), pp. 15–27.
RTA-2008-Toyama #lisp #proving #recursion #term rewriting #termination: Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations (YT), pp. 381–391.
RTA-2008-UrbanZ #proving: Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof (CU, BZ), pp. 409–424.
TAP-2008-ClaessenS #induction #proving: Finding Counter Examples in Induction Proofs (KC, HS), pp. 48–65.
DAC-2007-ChatterjeeMBK #equivalence #on the #proving: On Resolution Proofs for Combinational Equivalence (SC, AM, RKB, AK), pp. 600–605.
DATE-2007-KroeningS #image #interactive #proving #refinement #using #word: Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs (DK, NS), pp. 1325–1330.
VLDB-2007-LiYHK #authentication #query: Proof-Infused Streams: Enabling Authentication of Sliding Window Queries On Streams (FL, KY, MH, GK), pp. 147–158.
ITiCSE-2007-StallmannBRBGH #automaton #correctness #named #proving: ProofChecker: an accessible environment for automata theory correctness proofs (MFS, SB, RDR, SB, MCG, SDH), pp. 48–52.
ESOP-2007-BessonJT #abstract interpretation #proving: Small Witnesses for Abstract Interpretation-Based Proofs (FB, TPJ, TT), pp. 268–283.
ESOP-2007-FrancalanzaH #bisimulation #fault tolerance #proving: A Fault Tolerance Bisimulation Proof for Consensus (Extended Abstract) (AF, MH), pp. 395–410.
ESOP-2007-LiOS #compilation #higher-order #logic #set: Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic (GL, SO, KS), pp. 205–219.
STOC-2007-Dantchev #complexity #proving #rank: Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems (SSD), pp. 311–317.
STOC-2007-Lynch #algorithm #distributed #modelling #proving: Distributed computing theory: algorithms, impossibility results, models, and proofs (NAL), p. 247.
ICALP-2007-Damgard #encryption: A “proof-reading” of Some Issues in Cryptography (ID), pp. 2–11.
ICALP-2007-DershowitzT #complexity #proving: Complexity of Propositional Proofs Under a Promise (ND, IT), pp. 291–302.
SEFM-2007-FraserB #configuration management #proving #tool support: Configurable Proof Obligations in the Frog Toolkit (SF, RB), pp. 361–370.
SEFM-2007-Mehta #development #proving: Supporting Proof in a Reactive Development Environment (FM), pp. 103–112.
IFL-2007-HerhutSBGT #contract #dependent type #partial evaluation #proving #towards: From Contracts Towards Dependent Types: Proofs by Partial Evaluation (SH, SBS, RB, CG, KT), pp. 254–273.
AGTIVE-2007-MolEP #proving #reduction: A Single-Step Term-Graph Reduction System for Proof Assistants (MdM, MCJDvE, RP), pp. 184–200.
SIGAda-2007-Maurer #ada #proving #using: Using mathematics to improve ada compiled code, part 2: the proof (WDM), pp. 11–26.
PPDP-2007-Lucas #proving #termination: Practical use of polynomials over the reals in proofs of termination (SL), pp. 39–50.
SAC-2007-Dufourd #framework #proving #theorem: A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler’s formula (JFD), pp. 757–761.
SAC-2007-Hamid #memory management #runtime: Integrating a certified memory management runtime with proof-carrying code (NAH), pp. 1526–1533.
SAC-2007-Li #abstraction #parametricity #protocol #proving #verification: Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols (YL), pp. 1534–1535.
SAC-2007-ZhouHP #database #image #using: An additive-attack-proof watermarking mechanism for databases’ copyrights protection using image (XZ, MH, ZP), pp. 254–258.
CADE-2007-DeshaneHJLLM #encoding #first-order #proving #satisfiability: Encoding First Order Proofs in SAT (TD, WH, PJ, HL, CL, REM), pp. 476–491.
CADE-2007-Harrison #automation #proving #using: Automating Elementary Number-Theoretic Proofs Using Gröbner Bases (JH), pp. 51–66.
CADE-2007-VerchinineLP #automation #deduction #proving #verification: System for Automated Deduction (SAD): A Tool for Proof Verification (KV, AVL, AP), pp. 398–403.
CAV-2007-CohenN #proving #safety: Local Proofs for Global Safety Properties (AC, KSN), pp. 55–67.
CAV-2007-JhalaM #abstraction #array #proving: Array Abstractions from Proofs (RJ, KLM), pp. 193–206.
CSL-2007-Abramsky #geometry #interactive #proving: Full Completeness: Interactive and Geometric Characterizations of the Space of Proofs (Abstract) (SA), pp. 1–2.
CSL-2007-Beckmann #complexity #proving #source code: Proofs, Programs and Abstract Complexity (AB), pp. 4–5.
CSL-2007-Burel #bound #deduction: Unbounded Proof-Length Speed-Up in Deduction Modulo (GB), pp. 496–511.
CSL-2007-MillerN #proving: Incorporating Tables into Proofs (DM, VN), pp. 466–480.
CSL-2007-MillerS #composition #linear #logic #proving: From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic (DM, AS), pp. 405–419.
CSL-2007-NauroisM #correctness #exponential #multi #proving: Correctness of Multiplicative (and Exponential) Proof Structures is NL -Complete (PJdN, VM), pp. 435–450.
ICLP-2007-PettorossiPS #automation #correctness #logic programming #program transformation #proving: Automatic Correctness Proofs for Logic Program Transformations (AP, MP, VS), pp. 364–379.
LICS-2007-Nguyen #proving: Separating DAG-Like and Tree-Like Proof Systems (PN), pp. 235–244.
LICS-2007-RabinST #correctness #performance #proving: Highly Efficient Secrecy-Preserving Proofs of Correctness of Computations and Applications (MOR, RAS, CT), pp. 63–76.
MBT-2007-LedruBDA #case study #proving: A Case Study in Matching Test and Proof Coverage (YL, LdB, FD, FA), pp. 73–84.
RTA-2007-DowekH #proving: A Simple Proof That Super-Consistency Implies Cut Elimination (GD, OH), pp. 93–106.
RTA-2007-Kikuchi #calculus #normalisation #proving: Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi (KK), pp. 257–272.
SAT-2007-JussilaBSKW #proving #towards: A First Step Towards a Unified Proof Checker for QBF (TJ, AB, CS, DK, CMW), pp. 201–214.
TAP-2007-EngelH #generative #proving #testing: Generating Unit Tests from Formal Proofs (CE, RH), pp. 169–188.
TLCA-2007-Baillot #linear #logic #polynomial #type system: From Proof-Nets to Linear Logic Type Systems for Polynomial Time Computing (PB), pp. 2–7.
TLCA-2007-DavidN #calculus #equation #normalisation #proving #recursion: An Arithmetical Proof of the Strong Normalization for the λ -Calculus with Recursive Equations on Types (RD, KN), pp. 84–101.
TLCA-2007-Nakazawa #morphism #proving #reduction: An Isomorphism Between Cut-Elimination Procedure and Proof Reduction (KN), pp. 336–350.
ASE-2006-Futatsugi #proving #specification #verification: Verifying Specifications with Proof Scores in CafeOBJ (KF), pp. 3–10.
DAC-2006-RawatCKSGZS #named #proving #question: DFM: where’s the proof of value? (SR, RC, AK, JS, MG, NZ, AS), pp. 1061–1062.
TACAS-2006-FontaineMMNT #automation #interactive #proving #smt #towards: Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants (PF, JYM, SM, LPN, AFT), pp. 167–181.
TACAS-2006-LeueW #approach #graph #proving #termination: A Region Graph Based Approach to Termination Proofs (SL, WW), pp. 318–333.
PLDI-2006-CookPR #proving #termination: Termination proofs for systems code (BC, AP, AR), pp. 415–426.
STOC-2006-Gurvits #algorithm #approach #bound #proving: Hyperbolic polynomials approach to Van der Waerden/Schrijver-Valiant like conjectures: sharper bounds, simpler proofs and algorithmic applications (LG), pp. 417–426.
STOC-2006-Nordstrom #proving: Narrow proofs may be spacious: separating space and width in resolution (JN), pp. 507–516.
FLOPS-2006-BartheFPR #coq #proving #reasoning #recursion: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant (GB, JF, DP, VR), pp. 114–129.
CIAA-2006-OnderB #proving: XSLT Version 2.0 Is Turing-Complete: A Purely Transformation Based Proof (RO, ZB), pp. 275–276.
ICALP-v1-2006-KojevnikovI #bound #calculus #proving: Lower Bounds of Static Lovász-Schrijver Calculus Proofs for Tseitin Tautologies (AK, DI), pp. 323–334.
ICALP-v2-2006-CorinH #encryption #game studies #hoare #logic #probability #proving: A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs (RC, JdH), pp. 252–263.
FM-2006-SchellhornGHR #challenge #proving: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse (GS, HG, DH, WR), pp. 16–31.
ICFP-2006-Chlipala #composition #development #proving #verification: Modular development of certified program verifiers with a proof assistant (AC), pp. 160–171.
ICFP-2006-Shapiro #concurrent #proving #source code: Practical proofs of concurrent programs (MS), p. 123.
IFL-2006-Brady #proving: Ivor, a Proof Engine (EB), pp. 145–162.
LOPSTR-2006-MantelSK #data flow #proving #security #verification: Combining Different Proof Techniques for Verifying Information Flow Security (HM, HS, TK), pp. 94–110.
LOPSTR-2006-WinwoodKC #automation #monitoring #on the #synthesis: On the Automated Synthesis of Proof-Carrying Temporal Reference Monitors (SW, GK, MMTC), pp. 111–126.
PPDP-2006-Sulzmann #proving #source code: Extracting programs from type class proofs (MS), pp. 97–108.
POPL-2006-Dam #decidability #proving: Decidability and proof systems for language-based noninterference relations (MD), pp. 67–78.
POPL-2006-Leroy #certification #compilation #programming #proving: Formal certification of a compiler back-end or: programming a compiler with a proof assistant (XL), pp. 42–54.
RE-2006-Miller #development #modelling #proving #requirements: Proving the Shalls: Requirements, Proofs, and Model-Based Development (SPM), p. 261.
HPCA-2006-ConstantinidesPBZBMAO #architecture #named: BulletProof: a defect-tolerant CMP switch architecture (KC, SP, JAB, BZ, VB, SAM, TMA, MO), pp. 5–16.
HPDC-2006-BellenotBGIKPRBLRCF #named #parallel #proving: PROOF — The Parallel ROOT Facility (BB, RB, GG, JI, GK, AJP, FR, MB, CL, CR, PC, DF), pp. 379–380.
CAV-2006-BerdineCDO #automation #proving #source code #termination: Automatic Termination Proofs for Programs with Shape-Shifting Heaps (JB, BC, DD, PWO), pp. 386–400.
CSL-2006-ArtemovK #complexity #logic #proving: Logical Omniscience Via Proof Complexity (SNA, RK), pp. 135–149.
CSL-2006-GiamberardinoF #parallel #proving: Jump from Parallel to Sequential Proofs: Multiplicatives (PDG, CF), pp. 319–333.
IJCAR-2006-Boldo #algorithm #float #proving: Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms (SB), pp. 52–66.
IJCAR-2006-ConstableM #proving #semantics #source code: Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics (RLC, WM), pp. 162–176.
IJCAR-2006-GieslST #automation #dependence #framework #proving #termination: Automatic Termination Proofs in the Dependency Pair Framework (JG, PSK, RT), pp. 281–286.
IJCAR-2006-KozenKR #automation #category theory #proving: Automating Proofs in Category Theory (DK, CK, ER), pp. 392–407.
IJCAR-2006-NivelleM #finite #geometry #proving: Geometric Resolution: A Proof Procedure Based on Finite Model Search (HdN, JM), pp. 303–317.
IJCAR-2006-Werner #on the: On the Strength of Proof-Irrelevant Type Theories (BW), pp. 604–618.
LICS-2006-CoquandS #normalisation #proving #using: A Proof of Strong Normalisation using Domain Theory (TC, AS), pp. 307–316.
LICS-2006-Kozen #induction #probability #process #proving: Coinductive Proof Principles for Stochastic Processes (DK), pp. 359–366.
LICS-2006-Leivant #logic #proving #reasoning #source code: Matching Explicit and Modal Reasoning about Programs: A Proof Theoretic Delineation of Dynamic Logic (DL), pp. 157–168.
LICS-2006-MacielP #bound #composition #proving: Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives (AM, TP), pp. 189–200.
RTA-2006-Bruggink #finite #higher-order #product line #proving #using: A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property (HJSB), pp. 372–386.
RTA-2006-SantoFP #proving: Structural Proof Theory as Rewriting (JES, MJF, LP), pp. 197–211.
SAT-2006-Gelder #metric #proving: Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs (AVG), pp. 48–53.
SAT-2006-JussilaSB #proving #quantifier #satisfiability: Extended Resolution Proofs for Symbolic SAT Solving with Quantification (TJ, CS, AB), pp. 54–60.
SAT-2006-KojevnikovK #algebra #complexity #proving #strict: Complexity of Semialgebraic Proofs with Restricted Degree of Falsity (AK, ASK), pp. 11–21.
ICDAR-2005-RusuG #algorithm #interactive #proving #recognition #using: A Human Interactive Proof Algorithm Using Handwriting Recognition (AIR, VG), pp. 967–971.
ESOP-2005-CortierW #automation #protocol #proving #security: Computationally Sound, Automated Proofs for Security Protocols (VC, BW), pp. 157–171.
FASE-2005-FuriaRMM #automation #composition #proving #realtime: Automated Compositional Proofs for Real-Time Systems (CAF, MR, DM, AM), pp. 326–340.
FoSSaCS-2005-Cheney #logic #proving: A Simpler Proof Theory for Nominal Logic (JC), pp. 379–394.
TACAS-2005-LeinoMO #proving #quantifier #theorem proving: A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover (KRML, MM, XO), pp. 334–348.
IFL-2005-EekelenM #proving #strict #tool support: Proof Tool Support for Explicit Strictness (MCJDvE, MdM), pp. 37–54.
CHI-2005-ChellapillaLSC #design #interactive #proving: Designing human friendly human interaction proofs (HIPs) (KC, KL, PYS, MC), pp. 711–720.
SEKE-2005-OgataF #approach #liveness #proving #verification: Proof Score Approach to Verification of Liveness Properties (KO, KF), pp. 608–613.
POPL-2005-GrumbergLST #approximate #multi: Proof-guided underapproximation-widening for multi-process systems (OG, FL, OS, MT), pp. 122–131.
POPL-2005-LernerMRC #analysis #automation #data flow #proving: Automated soundness proofs for dataflow analyses and transformations via local rules (SL, TDM, ER, CC), pp. 364–377.
COCV-J-2005-BlechGLM #code generation #comparison #correctness #higher-order #optimisation #proving: Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL (JOB, SG, JL, SM), pp. 33–51.
COCV-J-2005-SalcianuA #analysis #correctness #data flow #proving: Machine-Checkable Correctness Proofs for Intra-procedural Dataflow Analyses (AS, KA), pp. 53–68.
CADE-2005-CastelliniS #first-order #logic #proving #theorem proving: Proof Planning for First-Order Temporal Logic (CC, AS), pp. 235–249.
CADE-2005-ContejeanC #first-order #logic #proving #similarity: Reflecting Proofs in First-Order Logic with Equality (EC, PC), pp. 7–22.
CADE-2005-McLaughlinH: A Proof-Producing Decision Procedure for Real Arithmetic (SM, JH), pp. 295–314.
CADE-2005-MeierM #multi #proving #theorem proving: System Description: Multi A Multi-strategy Proof Planner (AM, EM), pp. 250–254.
CSL-2005-CurienF: L-Nets, Strategies and Proof-Nets (PLC, CF), pp. 167–183.
CSL-2005-Perron #proving: A Propositional Proof System for Log Space (SP), pp. 509–524.
CSL-2005-Soltys #algorithm #matrix #proving: Feasible Proofs of Matrix Properties with Csanky’s Algorithm (MS), pp. 493–508.
ICLP-2005-SarkarPC #proving: Small Proof Witnesses for LF (SS, BP, KC), pp. 387–401.
LICS-2005-Hardin #algebra #proving: Proof Theory for Kleene Algebra (CH), pp. 290–299.
LICS-2005-Hofmann #approach: Proof-Theoretic Approach to Description-Logic (MH0), pp. 229–237.
RTA-2005-Felty #approach #semantics #tutorial: A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code (APF), pp. 394–406.
RTA-2005-NieuwenhuisO #congruence: Proof-Producing Congruence Closure (RN, AO), pp. 453–468.
RTA-2005-StumpT #algebra #proving #similarity: The Algebra of Equality Proofs (AS, LYT), pp. 469–483.
SAT-2005-Gelder #bound #distance #proving: Input Distance and Lower Bounds for Propositional Resolution Proof Length (AVG), pp. 282–293.
SAT-2005-HirschN #proving #simulation #strict: Simulating Cutting Plane Proofs with Restricted Degree of Falsity by Resolution (EAH, SIN), pp. 135–142.
TLCA-2005-DavidN #normalisation #proving #symmetry #λ-calculus #μ-calculus: Arithmetical Proofs of Strong Normalization Results for the Symmetric λμ-Calculus (RD, KN), pp. 162–178.
TLCA-2005-Felty #approach #semantics #tutorial: A Tutorial Example of the Semantic Approach to Foundational Proof-Carrying Code: Abstract (APF), p. 10.
TLCA-2005-Hayashi #game studies #proving #question: Can Proofs Be Animated By Games? (SH), pp. 11–22.
TLCA-2005-LamarcheS #logic #proving: Naming Proofs in Classical Propositional Logic (FL, LS), pp. 246–261.
TLCA-2005-PrevostoB #proving: Proof Contexts with Late Binding (VP, SB), pp. 324–338.
ESOP-2004-FilliatreL #proving #source code: Functors for Proofs and Programs (JCF, PL), pp. 370–384.
ESOP-2004-JiaW #distributed #proving #source code: Modal Proofs as Distributed Programs (Extended Abstract) (LJ, DW), pp. 219–233.
PEPM-2004-Morrisett #question #what: Invited talk: what’s the future for proof-carrying code? (JGM), p. 203.
PEPM-2004-PopeeaC #correctness #protocol #proving #type system #verification: A type system for resource protocol verification and its correctness proof (CP, WNC), pp. 135–146.
PLDI-2004-Appel #process #proving #revisited #social #source code #theorem: Social processes and proofs of theorems and programs, revisited (AWA), p. 170.
FLOPS-2004-Kikuchi #calculus #normalisation #proving: A Direct Proof of Strong Normalization for an Extended Herbelin?s Calculus (KK), pp. 244–259.
CIAA-2004-NishimuraY #automaton #finite #interactive #proving #quantum: An Application of Quantum Finite Automata to Interactive Proof Systems (HN, TY), pp. 225–236.
ICALP-2004-Meer #proving #theorem: Transparent Long Proofs: A First PCP Theorem for NPR (KM), pp. 959–970.
ICALP-2004-OstrovskyRS #commit #consistency #database #performance #proving #query: Efficient Consistency Proofs for Generalized Queries on a Committed Database (RO, CR, AS), pp. 1041–1053.
ICALP-2004-Razborov #proving: Feasible Proofs and Computations: Partnership and Fusion (AAR), pp. 8–14.
SEFM-2004-BeckertK #deduction #proving #reuse #verification: Proof Reuse for Deductive Program Verification (BB, VK), pp. 77–86.
KR-2004-EveraereKM #on the: On Merging Strategy-Proofness (PE, SK, PM), pp. 357–368.
SEKE-2004-WihartoS #logic #using #xml: Future Proofing and Retargeting Application Logic Using O2XML (MW, PS), pp. 173–178.
LOPSTR-2004-WellsY #graph #proving #synthesis: Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis (JBW, BY), pp. 262–277.
PPDP-2004-Morrisett #question #what: Invited talk: what’s the future for proof-carrying code? (JGM), p. 5.
POPL-2004-Benton #analysis #correctness #program transformation #proving #relational: Simple relational correctness proofs for static analyses and program transformations (NB), pp. 14–25.
POPL-2004-HenzingerJMM #abstraction #proving: Abstractions from proofs (TAH, RJ, RM, KLM), pp. 232–244.
RE-2004-KatzR #aspect-oriented #proving #requirements: From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems (SK, AR), pp. 48–57.
ICSE-2004-HaRCRD #case study #composition #experience #induction #proving #realtime: Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software: An Experience Report (VH, MR, DDC, HR, BD), pp. 304–313.
CAV-2004-Namjoshi #model checking: An Efficiently Checkable, Proof-Based Formulation of Vacuity in Model Checking (KSN), pp. 57–69.
CSL-2004-Hyland #abstract interpretation #calculus #proving: Abstract Interpretation of Proofs: Classical Propositional Calculus (MH), pp. 6–21.
CSL-2004-StrassburgerL #linear #logic #multi #on the #proving: On Proof Nets for Multiplicative Linear Logic with Units (LS, FL), pp. 145–159.
IJCAR-2004-GanzingerSW #composition #proving #similarity: Modular Proof Systems for Partial Functions with Weak Equality (HG, VSS, UW), pp. 168–182.
IJCAR-2004-MengP #interactive #proving #using: Experiments on Supporting Interactive Proof Using Resolution (JM, LCP), pp. 372–384.
IJCAR-2004-ThiemannGS #composition #dependence #proving #termination #using: Improved Modular Termination Proofs Using Dependency Pairs (RT, JG, PSK), pp. 75–90.
LICS-2004-Razborov #proving: Feasible Proofs and Computations: Partnership and Fusion (AAR), pp. 134–138.
LICS-2004-Terui #proving: Proof Nets and Boolean Circuits (KT), pp. 182–191.
RTA-2004-GieslTSF #automation #proving #termination: Automated Termination Proofs with AProVE (JG, RT, PSK, SF), pp. 210–220.
ASE-2003-EllisI #automation #exception #proving: Automation for Exception Freedom Proofs (BJE, AI), pp. 343–346.
DATE-2003-GoldbergN #proving #satisfiability #verification: Verification of Proofs of Unsatisfiability for CNF Formulas (EIG, YN), pp. 10886–10891.
DRR-2003-ChewB #interactive #named #proving: BaffleText: a human interactive proof (MC, HSB), pp. 305–316.
ESOP-2003-Ohori #proving: Register Allocation by Proof Transformation (AO), pp. 399–413.
FoSSaCS-2003-SprengerD #calculus #induction #on the #proving #reasoning #μ-calculus: On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μ-Calculus (CS, MD), pp. 425–440.
TACAS-2003-BerezinGD #linear #online: An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic (SB, VG, DLD), pp. 521–536.
TACAS-2003-GurfinkelC #proving: Proof-Like Counter-Examples (AG, MC), pp. 160–175.
TACAS-2003-Lee #case study #experience #what: What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code (PL0), p. 1.
STOC-2003-Friedman #proving: A proof of Alon’s second eigenvalue conjecture (JF), pp. 720–724.
ICALP-2003-MerroN #bisimulation #mobile #proving: Bisimulation Proof Methods for Mobile Ambients (MM, FZN), pp. 584–598.
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-RosuELM #equation #proving: Certifying and Synthesizing Membership Equational Proofs (GR, SE, PL, JM), pp. 359–380.
LOPSTR-2003-AlexandreBD #induction #proving #synthesis: Predicate Synthesis from Inductive Proof Attempt of Faulty Conjectures (FA, KB, MD), pp. 20–33.
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.
PPDP-2003-WuAS #proving: Foundational proof checkers with small witnesses (DW, AWA, AS), pp. 264–274.
CADE-2003-DeplagneKKN #equation #induction #proving #theorem: Proof Search and Proof Check for Equational and Inductive Theorems (ED, CK, HK, QHN), pp. 297–316.
CADE-2003-DixonF #named #prototype #proving #theorem proving: IsaPlanner: A Prototype Proof Planner in Isabelle (LD, JDF), pp. 279–283.
CADE-2003-Nivelle #axiom #first-order #proving: Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms (HdN), pp. 365–379.
CAV-2003-DongRS #model checking #proving: Evidence Explorer: A Tool for Exploring Model-Checking Proofs (YD, CRR, SAS), pp. 215–218.
CAV-2003-FlanaganJOS #lazy evaluation #proving #theorem proving #using: Theorem Proving Using Lazy Proof Explication (CF, RJ, XO, JBS), pp. 355–367.
CSL-2003-AndreoliM #concurrent: Concurrent Construction of Proof-Nets (JMA, LM), pp. 29–42.
CSL-2003-Iemhoff #proving #towards: Towards a Proof System for Admissibility (RI), pp. 255–270.
ICLP-2003-BruscoliG #logic programming #proving #tutorial: A Tutorial on Proof Theoretic Foundations of Logic Programming (PB, AG), pp. 109–127.
LICS-2003-HughesG #linear #logic #multi #proving: Proof Nets for Unit-free Multiplicative-Additive Linear Logic (Extended abstract) (DJDH, RJvG), pp. 1–10.
LICS-2003-MillerT #proving: A Proof Theory for Generic Judgments: An extended abstract (DM, AFT), pp. 118–127.
LICS-2003-Oliva #algorithm #effectiveness #polynomial #proving: Polynomial-time Algorithms from Ineffective Proofs (PO), pp. 128–137.
TLCA-2003-Montelatici #fixpoint #proving #semantics: Polarized Proof Nets with Cycles and Fixpoints Semantics (RM), pp. 256–270.
TLCA-2003-Oury #coq #equivalence #proving: Observational Equivalence and Program Extraction in the Coq Proof Assistant (NO), pp. 271–285.
VMCAI-2003-Namjoshi #abstraction #proving: Lifting Temporal Proofs through Abstractions (KSN), pp. 174–188.
DAC-2002-AnderssonBCH #approach #automation #design #problem #proving: A proof engine approach to solving combinational design automation problems (GA, PB, BC, ZH), pp. 725–730.
ESOP-2002-WandW #analysis #composition #proving: A Modular, Extensible Proof Method for Small-Step Flow Analyses (MW, GBW), pp. 213–227.
FoSSaCS-2002-Santocanale #calculus #category theory #proving #semantics: A Calculus of Circular Proofs and Its Categorical Semantics (LS), pp. 357–371.
STOC-2002-DworkS #proving: 2-round zero knowledge and proof auditors (CD, LJS), pp. 322–331.
STOC-2002-DziembowskiM #bound #proving #security: Tight security proofs for the bounded-storage model (SD, UMM), pp. 341–350.
ICALP-2002-GrigorievHP #algebra #bound #exponential #proving: Exponential Lower Bound for Static Semi-algebraic Proofs (DG, EAH, DVP), pp. 257–268.
FME-2002-Shankar #proving: Little Engines of Proof (NS), pp. 1–20.
FME-2002-Wildman #compilation #proving: A Formal Basis for a Program Compilation Proof Tool (LW), pp. 491–510.
IFM-2002-BarradasB #liveness #proving #specification: Specification and Proof of Liveness Properties under Fairness Assumptions in B Event Systems (HRB, DB), pp. 360–379.
IFL-2002-DowseSB #haskell #proving: Proving Make Correct: I/O Proofs in Haskell and Clean (MD, GS, AB), pp. 68–83.
ICEIS-2002-ViaeneBDVP #pattern matching #pattern recognition #proving #recognition #state of the art: Proof Running Two State-Of-The-Art Pattern Recognition Techniques in the Field of Direct Marketing (SV, BB, GD, JV, DVdP), pp. 446–454.
LOPSTR-2002-BossiFPR #data flow #proving #security: A Proof System for Information Flow Security (AB, RF, CP, SR), pp. 199–218.
PPDP-2002-FissoreGK #induction #proving #termination: System Presentation — CARIBOO: An induction based proof tool for termination with strategies (OF, IG, HK), pp. 62–73.
CADE-2002-Andreoli #middleware #paradigm: Focussing Proof-Net Construction as a Middleware Paradigm (JMA), pp. 501–516.
CADE-2002-Baaz #analysis #proving: Proof Analysis by Resolution (MB), pp. 517–532.
CADE-2002-BernardL #logic: Temporal Logic for Proof-Carrying Code (AB, PL), pp. 31–46.
CADE-2002-GalmicheM #logic #proving: Connection-Based Proof Search in Propositional BI Logic (DG, DM), pp. 111–128.
CADE-2002-Larchey-Wendling #logic: Combining Proof-Search and Counter-Model Construction for Deciding Gödel-Dummett Logic (DLW), pp. 94–110.
CADE-2002-SchneckN #approach #scalability: A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code (RRS, GCN), pp. 47–62.
CADE-2002-SiekmannBBCFFHKMMMNPSUWZ #development #proving: Proof Development with OMEGA (JHS, CB, VB, LC, AF, AF, HH, MK, AM, EM, MM, IN, MP, VS, CU, CPW, JZ), pp. 144–149.
CADE-2002-StumpD #framework #logic #performance #proving: Faster Proof Checking in the Edinburgh Logical Framework (AS, DLD), pp. 392–407.
CAV-2002-HenzingerJMNSW #proving: Temporal-Safety Proofs for Systems Code (TAH, RJ, RM, GCN, GS, WW), pp. 526–538.
CSL-2002-AtseriasB #on the #proving: On the Automatizability of Resolution and Related Propositional Proof Systems (AA, MLB), pp. 569–583.
CSL-2002-Beckmann #proving #strict: Resolution Refutations and Propositional Proofs with Height-Restrictions (AB), pp. 599–612.
CSL-2002-GeuversJ #interactive #logic #proving: Open Proofs and Open Terms: A Basis for Interactive Logic (HG, GIJ), pp. 537–552.
CSL-2002-HodasLPSP #logic programming #proving #resource management: A Tag-Frame System of Resource Management for Proof Search in Linear-Logic Programming (JSH, PL, JP, LS, EP), pp. 167–182.
CSL-2002-Nivelle #normalisation #proving: Extraction of Proofs from the Clausal Normal Form Transformation (HdN), pp. 584–598.
CSL-2002-Ogata #continuation #proving: A Proof Theoretical Account of Continuation Passing Style (IO), pp. 490–505.
ICLP-2002-Bruscoli #logic #proving: A Purely Logical Account of Sequentiality in Proof Search (PB), pp. 302–316.
ICLP-2002-Pientka #higher-order #logic programming: A Proof-Theoretic Foundation for Tabled Higher-Order Logic Programming (BP), pp. 271–286.
LICS-2002-Cook #complexity #proving: Complexity Classes, Propositional Proof Systems, and Formal Theories (SAC), p. 311.
LICS-2002-HamidSTMN #approach: A Syntactic Approach to Foundational Proof-Carrying Code (NAH, ZS, VT, SM, ZN), pp. 89–100.
LICS-2002-Shankar #proving: Little Engines of Proof (NS), p. 3–?.
LICS-2002-SoltysC #algebra #complexity #linear #proving: The Proof Complexity of Linear Algebra (MS, SAC), pp. 335–344.
SAT-2002-MotterM #on the #performance #proving #satisfiability: On proof systems behind efficient SAT solvers (DM, IM), p. 31.
VMCAI-2002-FocardiPR #bisimulation #data flow #proving #security: Proofs Methods for Bisimulation Based Information Flow Security (RF, CP, SR), pp. 16–31.
ASE-2001-CookIM #higher-order #proving #synthesis #theorem proving: Higher Order Function Synthesis Through Proof Planning (AC, AI, GM), pp. 307–310.
ESOP-2001-KatsumataO #decompiler #low level: Proof-Directed De-compilation of Low-Level Code (SyK, AO), pp. 352–366.
FoSSaCS-2001-BartheP #dependent type #morphism #proving #reuse #type system: Type Isomorphisms and Proof Reuse in Dependent Type Theory (GB, OP), pp. 57–71.
WCRE-2001-MycroftOK #decompiler #type system: Comparing Type-Based and Proof-Directed Decompilation (AM, AO, SyK), pp. 362–367.
STOC-2001-AchlioptasBM #complexity #proving: A sharp threshold in proof complexity (DA, PB, MSOM), pp. 337–346.
FLOPS-2001-Necula #architecture #scalability: A Scalable Architecture for Proof-Carrying Code (GCN), pp. 21–39.
DLT-2001-Razborov #complexity #proving: Proof Complexity of Pigeonhole Principles (AAR), pp. 100–116.
ICALP-2001-GoldreichVW #interactive #on the #proving: On Interactive Proofs with a Laconic Prover (OG, SPV, AW), pp. 334–345.
FME-2001-StoySA #correctness #protocol #proving: Proofs of Correctness of Cache-Coherence Protocols (JES, XS, A), pp. 43–71.
LOPSTR-2001-DelzannoE #debugging #logic programming #protocol #proving #security: Proof Theory, Transformations, and Logic Programming for Debugging Security Protocols (GD, SE), pp. 76–90.
LOPSTR-2001-FerrariFO #bound #logic #proving: Extracting Exact Time Bounds from Logical Proofs (MF, CF, MO), pp. 245–266.
IJCAR-2001-EglyS #composition #proving #source code: Deriving Modular Programs from Short Proofs (UE, SS), pp. 561–577.
IJCAR-2001-Fiedler #interactive #proving: P.rex: An Interactive Proof Explainer (AF), pp. 416–420.
IJCAR-2001-Larchey-WendlingMG #named #performance: STRIP: Structural Sharing for Efficient Proof-Search (DLW, DM, DG), pp. 696–700.
IJCAR-2001-Paulson #proving #set: SET Cardholder Registration: The Secrecy Proofs (LCP), pp. 5–12.
IJCAR-2001-SchmittLKN #interactive #proving #theorem proving: JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants (SS, LL, CK, AN), pp. 421–426.
IJCAR-2001-Stuber #modelling #proving: A Model-Based Completeness Proof of Extended Narrowing and Resolution (JS), pp. 195–210.
IJCAR-2001-Urbain #automation #incremental #proving #term rewriting #termination: Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems (XU), pp. 485–498.
LICS-2001-Appel: Foundational Proof-Carrying Code (AWA), pp. 247–256.
LICS-2001-Ganzinger #concept #decidability #problem #semantics #word: Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems (HG), pp. 81–90.
LICS-2001-Pfenning #proving #type system: Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory (FP), pp. 221–230.
RTA-2001-Hofbauer #proving #termination: Termination Proofs by Context-Dependent Interpretations (DH), pp. 108–121.
RTA-2001-VestergaardB #confluence #first-order #proving #using #λ-calculus: A Formalised First-Order Confluence Proof for the λ-Calculus Using One-Sorted Variable Names (RV, JB), pp. 306–321.
FoSSaCS-2000-CosmoKP #proving: Proof Nets and Explicit Substitutions (RDC, DK, EP), pp. 63–81.
FoSSaCS-2000-LinY #automaton #proving: A Proof System for Timed Automata (HL, WY), pp. 208–222.
TACAS-2000-Aspinall #development #proving: Proof General: A Generic Tool for Proof Development (DA0), pp. 38–42.
WRLA-2000-KirchnerG #normalisation #proving #termination: Termination and normalisation under strategy Proofs in ELAN (HK, IG), pp. 93–120.
STOC-2000-BihamBBMR #proving #quantum #security: A proof of the security of quantum key distribution (extended abstract) (EB, MB, POB, TM, VPR), pp. 715–724.
STOC-2000-CrescenzoSY #on the #proving: On zero-knowledge proofs (extended abstract): “from membership to decision” (GDC, KS, MY), pp. 255–264.
STOC-2000-KitaevW #exponential #interactive #parallel #proving #quantum #simulation: Parallelization, amplification, and exponential time simulation of quantum interactive proof systems (AK, JW), pp. 608–617.
STOC-2000-MacielPW #principle #proving: A new proof of the weak pigeonhole principle (AM, TP, ARW), pp. 368–377.
STOC-2000-Vadhan #complexity #interactive #on the #proving: On transformation of interactive proofs that preserve the prover’s complexity (SPV), pp. 200–207.
ICALP-2000-AielloBOR #performance #proving #verification: Fast Verification of Any Remote Procedure Call: Short Witness-Indistinguishable One-Round Proofs for NP (WA, SNB, RO, SR), pp. 463–474.
ICALP-2000-AtseriasGG #principle #proving: Monotone Proofs of the Pigeon Hole Principle (AA, NG, RG), pp. 151–162.
ICALP-2000-Moszkowski #logic #proving: An Automata-Theoretic Completeness Proof for Interval Temporal Logic (BCM), pp. 223–234.
ICALP-2000-SantisCP #proving: Necessary and Sufficient Assumptions for Non-iterative Zero-Knowledge Proofs of Knowledge for All NP Relations (ADS, GDC, GP), pp. 451–462.
WLC-2000-Shoji #proving #theorem: A Proof of Okninski, Putcha’s Theorem (KS), pp. 420–427.
TOOLS-ASIA-2000-WuJZ #design #implementation #normalisation #object-oriented #proving: Implementation and Proof for Normalization Design of Object-Oriented Data Schemes (YW, WJ, AZ), pp. 220–229.
LOPSTR-2000-PoernomoC #protocol #proving #source code: Protocols between programs and proofs (IP, JNC).
LOPSTR-J-2000-PoernomoC #protocol #proving #source code: Protocols between Programs and Proofs (IP, JNC), pp. 18–37.
PPDP-2000-Faggian #calculus #clustering #commutative #proving: Proof construction and non-commutativity: a cluster calculus (CF), pp. 80–91.
PPDP-2000-Gramlich #preprocessor #proving #term rewriting #termination: Simplifying termination proofs for rewrite systems by preprocessing (BG), pp. 139–150.
PPDP-2000-Necula #design #implementation: Proof-carrying code: design, implementation and applications (abstract) (GCN), pp. 175–177.
PPDP-2000-RoychoudhuryRR #proving #using: Justifying proofs using memo tables (AR, CRR, IVR), pp. 178–189.
PADL-2000-Lee: Production-Quality Proof-Carrying Code (PL0), p. 325.
POPL-2000-AppelF #semantics: A Semantic Model of Types and Machine Instuctions for Proof-Carrying Code (AWA, APF), pp. 243–253.
ICSE-2000-KeidarKLS #incremental #proving #simulation: An inheritance-based technique for building simulation proofs incrementally (IK, RK, NAL, AAS), pp. 478–487.
CADE-2000-BezemHN #automation #proving #type system #using: Automated Proof Construction in Type Theory Using Resolution (MB, DH, HdN), pp. 148–163.
CADE-2000-JacksonL #interactive #proving: System Description: Interactive Proof Critics in XBarnacle (MJ, HL), pp. 502–506.
CADE-2000-Meier #proving: System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level (AM), pp. 460–464.
CADE-2000-NeculaL #generative #proving #theorem proving: Proof Generation in the Touchstone Theorem Prover (GCN, PL), pp. 25–44.
CAV-2000-ColbyLN #architecture #java: A Proof-Carrying Code Architecture for Java (CC, PL, GCN), pp. 557–560.
CL-2000-HarlandLW #logic #multi #proving: Goal-Directed Proof Search in Multiple-Conclusions Intuitionistic Logic (JH, TL, MW), pp. 254–268.
CL-2000-MelisM #multi #proving #theorem proving: Proof Planning with Multiple Strategies (EM, AM), pp. 644–659.
CSL-2000-BaazZ #fuzzy #logic #proving: Hypersequent and the Proof Theory of Intuitionistic Fuzzy Logic (MB, RZ), pp. 187–201.
CSL-2000-Yavorsky #logic #on the #proving #standard: On the Logic of the Standard Proof Predicate (REY), pp. 527–541.
LICS-2000-MurawskiO #performance #proving #verification: Dominator Trees and Fast Verification of Proof Nets (ASM, CHLO), pp. 181–191.
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.
WICSA-1999-Riemenschneider #architecture #correctness: Checking the Correctness of Architectural Transformation Steps via Proof-Carrying Architectures (RAR), pp. 65–82.
ASE-1999-FedeleK #automation #proving: Automatic Proofs of Properties of Simple C-- Modules (CF, EK), pp. 283–286.
ASE-1999-StarkI #automation #imperative #proving #synthesis #theorem proving #towards: Towards Automatic Imperative Program Synthesis Through Proof Planning (JS, AI), pp. 44–51.
ASE-1999-WhittleBBL #editing #ml: An ML Editor Based on Proofs-As-Programs (JW, AB, RJB, HL), pp. 166–173.
TACAS-1999-HickeyLR #proving #specification: Specifications and Proofs for Ensemble Layers (JH, NAL, RvR), pp. 119–133.
STOC-1999-Ben-SassonW #proving: Short Proofs are Narrow — Resolution Made Simple (EBS, AW), pp. 517–526.
STOC-1999-KlivansM #graph #morphism #polynomial #proving: Graph Nonisomorphism has Subexponential Size Proofs Unless the Polynomial-Time Hierarchy Collapses (AK, DvM), pp. 659–667.
ICALP-1999-ComptonD #encryption #protocol #proving: Proof Techniques for Cryptographic Protocols (KJC, SD), pp. 25–39.
ICALP-1999-Miculan #calculus #formal method #induction #lazy evaluation #proving #μ-calculus: Formalizing a Lazy Substitution Proof System for μ-calculus in the Calculus of Inductive Constructions (MM), pp. 554–564.
ICALP-1999-Szegedy #artificial reality #logic #proving: Many-Valued Logics and Holographic Proofs (MS), pp. 676–686.
FM-v1-1999-MoninK #algorithm #consistency #correctness #proving #standard: Correctness Proof of the Standardized Algorithm for ABR Conformance (JFM, FK), pp. 662–681.
FM-v2-1999-KingHCP #experience #industrial #proving #verification: The Value of Verification: Positive Experience of Industrial Proof (SK, JH, RC, AP), pp. 1527–1545.
FM-v2-1999-Moreira #component #proving: Proof Preservation in Component Generalization (AMM), p. 1866.
FM-v2-1999-RandimbivololonaSBPRS #approach #proving: Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach (FR, JS, PB, AP, JR, DS), pp. 1798–1815.
IFM-1999-Hennessy #calculus #message passing #process #proving: Proof Systems for Message-Passing Process Calculi (MH), p. 26.
ICFP-1999-Crary #parametricity #proving: A Simple Proof Technique for Certain Parametricity Results (KC), pp. 82–89.
ICFP-1999-ZdancewicGM #programming language #proving: Principals in Programming Languages: A Syntactic Proof Technique (SZ, DG, JGM), pp. 197–207.
AGTIVE-1999-MolE #prototype #proving: A Proof Tool Dedicated to Clean — The First Prototype (MdM, MCJDvE), pp. 271–278.
LOPSTR-1999-DucasseR #consistency #formal method #proving: Proof Obligations of the B Formal Method: Local Proofs Ensure Global Consistency (MD, LR), pp. 10–29.
PPDP-1999-KamareddineM #on the #proving #recursion #termination: On Formalised Proofs of Termination of Recursive Functions (FK, FM), pp. 29–46.
PPDP-1999-VerbaetenSS #composition #prolog #proving #termination: Modular Termination Proofs for Prolog with Tabling (SV, KFS, DDS), pp. 342–359.
PADL-1999-Lai #constraints #debugging #proving #using: Using Constraints in Local Proofs for CLP Debugging (CL), pp. 350–359.
CADE-1999-Horacek #proving: Presenting Proofs in a Human-Oriented Way (HH), pp. 142–156.
CADE-1999-Lopes #automation #generative #higher-order #logic #proving: Automatic Generation of Proof Search Strategies for Second-order Logic (RHCL), pp. 414–428.
CAV-1999-GlusmanK #equivalence #proving: Mechanizing Proofs of Computation Equivalence (MG, SK), pp. 354–367.
CSL-1999-GeuversPZ #proving #type system: Safe Proof Checking in Type Theory with Y (HG, EP, JZ), pp. 439–452.
CSL-1999-Roversi #logic #proving: A P-Time Completeness Proof for Light Logics (LR), pp. 469–483.
LICS-1999-BorealeNP #encryption #process #proving: Proof Techniques for Cryptographic Processes (MB, RDN, RP), pp. 157–166.
LICS-1999-Guerrini #correctness #linear #multi #proving: Correctness of Multiplicative Proof Nets Is Linear (SG), pp. 454–463.
RTA-1999-CosmoG #normalisation #proving: Strong Normalization of Proof Nets Modulo Structural Congruences (RDC, SG), pp. 75–89.
TLCA-1999-Laurent: Polarized Proof-Nets: Proof-Nets for LC (OL), pp. 213–227.
FASE-1998-BerregebBR #proving: Observational Proofs with Critical Contexts (NB, AB, MR), pp. 38–53.
TACAS-1998-JensenL #abstraction #algorithm #proving #using: A Proof of Burns N-Process Mutual Exclusion Algorithm Using Abstraction (HEJ, NAL), pp. 409–423.
STOC-1998-BeameKPS #complexity #on the #proving #random #satisfiability: On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas (PB, RMK, TP, MES), pp. 561–571.
ICALP-1998-Barthe: The Relevance of Proof-Irrelevance (GB), pp. 755–768.
ICALP-1998-GrafV #proving: Reducing Simple Polygons to Triangles — A Proof for an Improved Conjecture (TG, KV), pp. 130–139.
ICALP-1998-Lin #proving #π-calculus: Complete Proof Systems for Observation Congruences in Finite-Control π-Calculus (HL), pp. 443–454.
ECOOP-1998-FerreiraS #algorithm #correctness #distributed #garbage collection #modelling #proving: Modelling a Distributed Cached Store for Garbage Collection: The Algorithm and Its Correctness Proof (PF, MS), pp. 234–259.
ALP-PLILP-1998-LeviV #abstract interpretation #proving: Derivation of Proof Methods by Abstract Interpretation (GL, PV), pp. 102–117.
LOPSTR-1998-Richardson #named #proving #theorem proving: Abstract: Proof Planning with Program Schemas (JR), pp. 313–315.
LOPSTR-1998-StarkI #invariant #proving: Invariant Discovery via Failed Proof Attempts (JS, AI), pp. 271–288.
POPL-1998-Blanchet #analysis #correctness #implementation #proving: Escape Analysis: Correctness Proof, Implementation and Experimental Results (BB), pp. 25–37.
FSE-1998-FongC #architecture #composition #mobile #proving #verification: Proof Linking: An Architecture for Modular Verification of Dynamically-Linked Mobile Code (PWLF, RDC), pp. 222–230.
CADE-1998-KreitzHH #communication #development #proving: A Proof Environment for the Development of Group Communication Systems (CK, MH, JH), pp. 317–332.
CADE-1998-RichardsonSG #higher-order #logic #proving #theorem proving: System Description: Proof Planning in Higher-Order Logic with Lambda-Clam (JR, AS, IG), pp. 129–133.
CAV-1998-Bolignano #encryption #model checking #protocol #verification: Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols (DB), pp. 77–87.
CAV-1998-HosabettuSG #correctness #pipes and filters #proving: Decomposing the Proof of Correctness of pipelined Microprocessors (RH, MKS, GG), pp. 122–134.
CAV-1998-Moore #proving: An ACL2 Proof of Write Invalidate Cache Coherence (JSM), pp. 29–38.
CAV-1998-Wilding #policy #proving #realtime #scheduling: A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy (MW), pp. 369–378.
JICSLP-1998-Cervesato #compilation #logic programming: Proof-Theoretic Foundation of Compilation in Logic Programming (IC), pp. 115–129.
LICS-1998-JohannsenP #on the #proving: On Proofs about Threshold Circuits and Counting Hierarchies (JJ, CP), pp. 444–452.
LICS-1998-NeculaL #performance #proving #representation #validation: Efficient Representation and Validation of Proofs (GCN, PL), pp. 93–104.
RTA-1998-Comon #consistency #proving: About Proofs by Consistency (Abstract) (HC), pp. 136–137.
RTA-1998-Xi #automation #proving #termination #towards: Towards Automated Termination Proofs through “Freezing” (HX), pp. 271–285.
ASE-1997-ArmandoSG #automation #paradigm #recursion #source code #synthesis: Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm (AA, AS, IG), pp. 2–9.
ASE-1997-Caldwell: Moving Proofs-As-Programs into Practice (JLC), pp. 10–17.
STOC-1997-CramerD #linear #performance #proving: Linear Zero-Knowledge — A Note on Efficient Zero-Knowledge Proofs and Arguments (RC, ID), pp. 436–445.
STOC-1997-KilianPT #proving: Probabilistically Checkable Proofs with Zero Knowledge (JK, EP, GT), pp. 496–505.
STOC-1997-MacielP #on the #proving: On ACC0[pk] Frege Proofs (AM, TP), pp. 720–729.
STOC-1997-Mulmuley #algebra #exclamation #proving: Is There an Algebraic Proof for P != NC? (Extended Abstract) (KM), pp. 210–219.
STOC-1997-RazborovWY #branch #calculus #proving #source code: Read-Once Branching Programs, Rectangular Proofs of the Pigeonhole Principle and the Transversal Calculus (AAR, AW, ACCY), pp. 739–748.
ICALP-1997-Fu #approach #communication #proving: A Proof Theoretical Approach to Communication (YF), pp. 325–335.
FME-1997-AichernigL #generative #proving: A Proof Obligation Generator for VDM-SL (BKA, PGL), pp. 338–357.
FME-1997-BoerHR #composition #concurrent #proving: A Compositional Proof System for Shared Variable Concurrency (FSdB, UH, WPdR), pp. 515–532.
FME-1997-Gregoire #protocol #proving #using: TLA + PROMELA: Conjecture, Check, Proof, Engineering New Protocols Using Methods and Formal Notations (JCG), pp. 378–397.
ALP-1997-CairesM #proving #semantics: Proof Net Semantics of Proof Search Computation (LC, LM), pp. 194–208.
POPL-1997-Necula: Proof-Carrying Code (GCN), pp. 106–119.
POPL-1997-Sands #functional #proving: From SOS Rules to Proof Principles: An Operational Metatheory for Functional Languages (DS), pp. 428–441.
CADE-1997-BornatS #named: Jape: A Calculator for Animating Proof-on-Paper (RB, BS), pp. 412–415.
CADE-1997-DefourneauxP #proving: Partial Matching for Analogy Discovery in Proofs and Counter-Examples (GD, NP), pp. 431–445.
CADE-1997-DennisBG #bisimulation #induction #proving #using: Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs (LAD, AB, IG), pp. 276–290.
CADE-1997-EastaughffeOC #formal method #proving #state machine #visual notation: Proof Tactics for a Theory of State Machines in a Graphical Environment (KAE, MAO, AC), pp. 366–379.
CADE-1997-KreitzMOS #linear #logic #proving: Connection-Based Proof Construction in Linear Logic (CK, HM, JO, SS), pp. 207–221.
CADE-1997-OheimbG #algebra #named #proving: RALL: Machine-Supported Proofs for Relation Algebra (DvO, TFG), pp. 380–394.
CADE-1997-WolfS #named #natural language #proving: ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output (AW, JS), pp. 61–64.
CSL-1997-CoquandP #problem: A Proof-Theoretical Investigation of Zantema’s Problem (TC, HP), pp. 177–188.
CSL-1997-Faggian #logic #proving: Classical Proofs via Basic Logic (CF), pp. 203–219.
LICS-1997-CosmoK #normalisation #proving: Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (Extended Abstract) (RDC, DK), pp. 35–46.
TLCA-1997-GuerriniMM #proving: Proof Nets, Garbage, and Computations (SG, SM, AM), pp. 181–195.
TACAS-1996-Lamport #proving: Managing Proofs (Abstract) (LL), p. 34.
SAS-1996-MullerGS #automation #composition #prolog #proving #source code #termination: Automated Modular Termination Proofs for Real Prolog Programs (MM, TG, KS), pp. 220–237.
STOC-1996-CleggEI #algorithm #proving #satisfiability #using: Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability (MC, JE, RI), pp. 174–183.
STOC-1996-Fu #composition #proving: Modular Coloring Formulas Are Hard for Cutting Planes Proofs (XF), pp. 595–602.
STOC-1996-Okamoto #on the #proving #statistics: On Relationships between Statistical Zero-Knowledge Proofs (TO), pp. 649–658.
ICALP-1996-Razborov #bound #independence #proving: Lower Bounds for Propositional Proofs and Independence Results in Bounded Arithmetic (AAR), pp. 48–62.
FME-1996-Hoare #how #proving #question #reliability: How Did Software Get So Reliable Without Proof? (CARH), pp. 1–17.
ALP-1996-Volpe #abstraction #proving: Abstractions of Uniform Proofs (PV), pp. 224–237.
LOPSTR-1996-DungKT #proving #reasoning #synthesis: Synthesis of Proof Procedures for Default Reasoning (PMD, RAK, FT), pp. 313–324.
ICSE-1996-Hoare #how #proving #reliability: The Role of Formal Techniques: Past, Current and Future or How Did Software Get so Reliable without Proof? (Extended Abstract) (CARH), pp. 233–234.
CADE-1996-Felty #calculus #proving #set: Proof Search with Set Variable Instantiation in the Calculus of Constructions (APF), pp. 658–672.
CADE-1996-Fuchs #experience #heuristic #proving: Experiments in the Heuristic Use of Past Proof Experience (MF), pp. 523–537.
CADE-1996-GiunchigliaV #abstraction #named #proving: ABSFOL: A Proof Checker with Abstraction (FG, AV), pp. 136–140.
CADE-1996-Harrison #optimisation #proving: Optimizing Proof Search in Model Elimination (JH), pp. 313–327.
CADE-1996-HuangF #proving: Presenting Machine-Found Proofs (XH, AF), pp. 221–225.
CADE-1996-IrelandB #induction #proving: Extensions to a Generalization Critic for Inductive Proof (AI, AB), pp. 47–61.
CADE-1996-Nipkow #higher-order #proving: More Church-Rosser Proofs (in Isabelle/HOL) (TN), pp. 733–747.
CADE-1996-RitterPW: Proof-Terms for Classical and Intuitionistic Resolution (Extended Abstract) (ER, DJP, LAW), pp. 17–31.
CADE-1996-SchmittK #matrix #proving: Converting Non-Classical Matrix Proofs into Sequent-Style Systems (SS, CK), pp. 418–432.
CADE-1996-Voronkov #logic #similarity: Proof-Search in Intuitionistic Logic with Equality, or Back to Simultaneous Rigid E-Unification (AV), pp. 32–46.
CAV-1996-OwreRRSS #model checking #named #proving #specification: PVS: Combining Specification, Proof Checking, and Model Checking (SO, SR, JMR, NS, MKS), pp. 411–414.
CSL-1996-Malecki #proving: Proofs in System Fω Can Be Done in System Fω¹ (SM), pp. 297–315.
JICSLP-1996-Thielscher #logic programming #proving #semantics #source code: A Nonmonotonic Disputation-Based Semantics and Proof Procedure for Logic Programs (MT), pp. 483–497.
LICS-1996-Ong #category theory #proving #semantics: A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations (Preliminary Extended Abstract) (CHLO), pp. 230–241.
RTA-1996-BerregebBR #commutative #induction #named #proving: SPIKE-AC: A System for Proofs by Induction in Associative-Commutative Theories (NB, AB, MR), pp. 428–431.
RTA-1996-GuerriniMM #proving: Coherence for Sharing Proof Nets (SG, SM, AM), pp. 215–229.
RTA-1996-Huet #design #proving: Design Proof Assistant (Abstract) (GPH), p. 153.
RTA-1996-Luth #algebra #composition #proving #term rewriting #theorem: Compositional Term Rewriting: An Algebraic Proof of Toyama’s Theorem (CL), pp. 261–275.
RTA-1996-Voisin #interface #proving: A New Proof Manager and Graphic Interface for Larch Prover (FV), pp. 408–411.
FPLE-1995-HartelET #proving #student: Basic Proof Skills of Computer Science Students (PHH, BvE, DT), pp. 269–287.
TACAS-1995-LarsenSW #constraints #proving: A Constraint Oriented Proof Methodology Based on Modal Transition Systems (KGL, BS, CW), pp. 17–40.
STOC-1995-BonetPR #bound #proving: Lower bounds for cutting planes proofs with small coefficients (MLB, TP, RR), pp. 575–584.
STOC-1995-FeigeK #proving #random: Impossibility results for recycling random bits in two-prover proof systems (UF, JK), pp. 457–468.
ICML-1995-Fuchs #adaptation #heuristic #learning #parametricity #proving: Learning Proof Heuristics by Adaptive Parameters (MF), pp. 235–243.
LOPSTR-1995-KreitzOS #development #proving: Guiding Program Development Systems by a Connection Based Proof Strategy (CK, JO, SS), pp. 137–151.
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.
ESEC-1995-Coen-PorisiniKM #framework #proving: A Formal Framework for ASTRAL Inter-level Proof Obligations (ACP, RAK, DM), pp. 90–108.
ASF+SDF-1995-NaidichD #asf+sdf #automation #induction #proving #specification: Specifying an Automated Induction Proof Procedure in ASF+SDF (DN, TBD), pp. 233–254.
CAV-1995-RajanSS #automation #integration #model checking #proving: An Integration of Model Checking with Automated Proof Checking (SR, NS, MKS), pp. 84–97.
ILPS-1995-FerrandL #composition #correctness #logic programming #proving #source code: A Compositional Proof Method of Partial Correctness for Normal Logic Programs (GF, AL), pp. 209–223.
ILPS-1995-Hui-Bon-Hoa #proving: Clause-based proofs for hereditary Harrop formulas (AHBH), pp. 179–193.
LICS-1995-Dutertre #first-order #logic #proving: Complete Proof Systems for First Order Interval Temporal Logic (BD), pp. 36–43.
LICS-1995-KestenP #proving: A Complete Proof Systems for QPTL (YK, AP), pp. 2–12.
LICS-1995-KfouryW #normalisation #proving #reduction #semantics #λ-calculus: New Notions of Reduction and Non-Semantic Proofs of β-Strong Normalization in Typed λ-Calculi (AJK, JBW), pp. 311–321.
LICS-1995-NadathurL #logic programming #proving: Uniform Proofs and Disjunctive Logic Programming (Extended Abstract) (GN, DWL), pp. 148–155.
RTA-1995-Giesl #generative #order #polynomial #proving #termination: Generating Polynomial Orderings for Termination Proofs (JG), pp. 426–431.
RTA-1995-Kahrs #proving #termination #towards: Towards a Domain Theory for Termination Proofs (SK), pp. 241–255.
RTA-1995-Nieuwenhuis #constraints #on the #proving: On Narrowing, Refutation Proofs and Constraints (RN), pp. 56–70.
RTA-1995-Steinbach #automation #order #proving #termination: Automatic Termination Proofs With Transformation Orderings (JS), pp. 11–25.
TLCA-1995-CoscoyKT #proving: Extracting Text from Proofs (YC, GK, LT), pp. 109–123.
TLCA-1995-Leclerc #coq #development #multi #order #proving #term rewriting #termination: Termination Proof of Term Rewriting System with the Multiset Path Ordering. A Complete Development in the System Coq (FL), pp. 312–327.
TLCA-1995-PolS #proving #strict #termination: Strict Functionals for Termination Proofs (JvdP, HS), pp. 350–364.
ESOP-J-1992-Henglein94 #dynamic typing #proving #syntax #type system: Dynamic Typing: Syntax and Proof Theory (FH), pp. 197–230.
ESOP-1994-Walker #algebra #proving: Algebraic Proofs of Properties of Objects (DW), pp. 501–516.
STOC-1994-BellareGLR #approximate #performance #probability #proving: Efficient probabilistic checkable proofs and applications to approximation (MB, SG, CL, AR), p. 820.
STOC-1994-PolishchukS #artificial reality #proving: Nearly-linear size holographic proofs (AP, DAS), pp. 194–203.
STOC-1994-RazborovR #proving: Natural proofs (AAR, SR), pp. 204–213.
FME-1994-Ledru #development #specification: Proof-Based Development of Specifications with KIDS/VDM (YL), pp. 214–232.
LFP-1994-Cosmadakis #algebra #proving: Complete Proof Systems for Algebraic Simply-Typed Terms (SSC), pp. 220–226.
TRI-Ada-1994-BellBHKKLMOSTWZ #concept #design #reliability #reuse: Software design for reliability and reuse: a proof-of-concept demonstration (JMB, FB, JH, RBK, AK, JL, LM, DO, TS, LT, LW, TZ), pp. 396–404.
KR-1994-AttardiS #proving: Proofs in Context (GA, MS), pp. 15–26.
ALP-1994-Bouhoula #induction #proving: Sufficient Completeness and Parameterized Proofs by Induction (AB), pp. 23–40.
ALP-1994-Volpe #concurrent #linear #logic programming #proving: Concurrent Logic Programming as Uniform Linear Proofs (PV), pp. 133–149.
LOPSTR-1994-AttardiS #proving: Building Proofs in Context (GA, MS), pp. 410–424.
CADE-1994-Anderson #optimisation #proving #representation: Representing Proof Transformations for Program Optimizations (PA), pp. 575–589.
CADE-1994-Bouhoula #induction #named #proving: SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs (AB), pp. 836–840.
CADE-1994-ChazarainK #induction #proving: Mechanizable Inductive Proofs for a Class of Forall Exists Formulas (JC, EK), pp. 118–132.
CADE-1994-FarmerGNT #proving: Proof Script Pragmatics in IMPS (WMF, JDG, MEN, FJT), pp. 356–370.
CADE-1994-FeltyH #proving #theorem proving: Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables (APF, DJH), pp. 605–619.
CADE-1994-Huang #proving #re-engineering: Reconstruction Proofs at the Assertion Level (XH), pp. 738–752.
CADE-1994-HuangKKMNRS #development #named #proving: Omega-MKRP: A Proof Development Environment (XH, MK, MK, EM, DN, JR, JHS), pp. 788–792.
CADE-1994-Hutter #induction #order #proving #synthesis: Synthesis of Induction Orderings for Existence Proofs (DH), pp. 29–41.
CADE-1994-Lysne #consistency #on the #proving: On the Connection between Narrowing and Proof by Consistency (OL), pp. 133–147.
CADE-1994-Platek #proving #what: What is a Proof? (Abstract) (RP), p. 431.
CADE-1994-Portoraro #automation #named #proving: Symlog: Automated Advice in Fitch-style Proof Construction (FDP), pp. 802–806.
CADE-1994-RichardsKSW #logic #named: Mollusc: A General Proof-Development Shell for Sequent-Based Logics (BLR, IK, AS, GAW), pp. 826–830.
ICLP-1994-Pedreschi #prolog #proving #runtime #source code: A Proof Method for Runtime Properties of Prolog Programs (DP), pp. 584–598.
LICS-1994-AndersenSW #calculus #composition #proving #μ-calculus: A Compositional Proof System for the Modal μ-Calculus (HRA, CS, GW), pp. 144–153.
LICS-1994-BaazFL #proving: A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation (MB, CGF, AL), pp. 213–219.
LICS-1994-Burstall #proving #refinement: Terms, Proofs, and Refinement (Extended abstract) (RMB), pp. 2–7.
LICS-1994-HofmannS #proving: The Groupoid Model Refutes Uniqueness of Identity Proofs (MH, TS), pp. 208–212.
LICS-1994-ImpagliazzoPU #bound #proving: Upper and Lower Bounds for Tree-Like Cutting Planes Proofs (RI, TP, AU), pp. 220–228.
LICS-1994-LincolnS #calculus #first-order #linear #logic #proving: Proof Search in First-Order Linear Logic and Other Cut-Free Sequent Calculi (PL, NS), pp. 282–291.
PEPM-1993-Lawall #induction #partial evaluation #proving #using: Proofs by Structural Induction using Partial Evaluation (JLL), pp. 155–166.
STOC-1993-BellareGLR #approximate #performance #proving: Efficient probabilistically checkable proofs and applications to approximations (MB, SG, CL, AR), pp. 294–304.
STOC-1993-CoffmanJSW #analysis #markov #proving: Markov chains, computer proofs, and average-case analysis of best fit bin packing (EGCJ, DSJ, PWS, RRW), pp. 412–421.
FME-1993-BrownM #concurrent #proving #source code: A Proof Environment for Concurrent Programs (NB, DM), pp. 196–215.
LOPSTR-1993-LombartWD #proving #synthesis: Guiding Synthesis Proofs (VL, GAW, YD), pp. 67–81.
LOPSTR-1993-MaddenHGB #automation #generative #performance #proving #source code #theorem proving: A General Technique for Automatically Generating Efficient Programs Through the Use of Proof Planning (Abstract) (PM, JH, IG, AB), pp. 64–66.
LOPSTR-1993-ProiettiP #proving #source code #synthesis: Synthesis of Programs from Unfold/Fold Proofs (MP, AP), pp. 141–158.
ESEC-1993-Coen-PorisiniM #framework #proving: A Formal Framework for ASTRAL Intra-Level Proof Obligations (ACP, DM), pp. 483–500.
CAV-1993-Sogaard-AndersenGGLP #proving #simulation: Computer-Assisted Simulation Proofs (JFSA, SJG, JVG, NAL, AP), pp. 305–319.
CSL-1993-BaazZ #equivalence #proving #using: Short Proofs of Tautologies Using the Schema of Equivalence (MB, RZ), pp. 33–35.
CSL-1993-SiegW #program transformation #proving: Program Transformation and Proof Transformation (WS, SSW), pp. 305–317.
ILPS-1993-BarbackL #proving: A Proof Procedure for Default Theories with Extensions (MDB, JL), p. 651.
ILPS-1993-Teusink #logic programming #proving #source code: A Proof Procedure for Extended Logic Programs (FT), pp. 235–249.
TLCA-1993-Altenkirch #formal method #normalisation #proving #system f: A Formalization of the Strong Normalization Proof for System F in LEGO (TA), pp. 13–28.
TLCA-1993-Berger #normalisation #proving: Program Extraction from Normalization Proofs (UB0), pp. 91–106.
TLCA-1993-HylandO #normalisation #proving: Modified Realizability Toposes and Strong Normalization Proofs (JMEH, CHLO), pp. 179–194.
STOC-1992-DorT #composition #graph #proving: Graph Decomposition Is NPC-A Complete Proof of Holyer’s Conjecture (DD, MT), pp. 252–263.
STOC-1992-FeigeL92a #problem #proving: Two-Prover One-Round Proof Systems: Their Power and Their Problems (Extended Abstract) (UF, LL), pp. 733–744.
STOC-1992-Kilian #performance #proving: A Note on Efficient Zero-Knowledge Proofs and Arguments (Extended Abstract) (JK), pp. 723–732.
ICALP-1992-SantisPY #bound #proving #statistics #verification: One-Message Statistical Zero-Knowledge Proofs and Space-Bounded Verifier (ADS, GP, MY), pp. 28–40.
SEKE-1992-KaoH #graph #logic #proving #realtime: A Graph Proof Procedure for Real Time Logic (JHK, LJH), pp. 300–306.
ALP-1992-Lysne #algebra #consistency #proving #semantics: Proof by Consistency in Constructive Systems with Final Algebra Semantics (OL), pp. 276–290.
LOPSTR-1992-KraanBB #logic programming #proving #synthesis #theorem proving: Logic Program Synthesis via Proof Planning (IK, DAB, AB), pp. 1–14.
LOPSTR-1992-Ornaghi #proving: Proof Nets (MO), pp. 61–79.
CADE-1992-Ammon #analysis #automation #logic #proving: Automatic Proofs in Mathematical Logic and Analysis (KA), pp. 4–19.
CADE-1992-BoyerY #automation #correctness #proving #source code: Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor (RSB, YY), pp. 416–430.
CADE-1992-CaferraD #logic #proving #semantics: Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic (RC, SD), pp. 385–399.
CADE-1992-ChirimarGI #interface #named #performance #proving #visual notation: Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof Checker (JC, CAG, MVI), pp. 711–715.
CADE-1992-Madden #automation #optimisation #proving: Automatic Program Optimization Through Proof Transformation (PM), pp. 446–460.
CADE-1992-Shankar #calculus #proving: Proof Search in the Intuitionistic Sequent Calculus (NS), pp. 522–536.
CADE-1992-UribeFM #automation #bibliography #framework #proving: An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure Systems (TEU, AMF, MKM), pp. 721–725.
CADE-1992-WalshNB #proving #theorem proving: The Use of Proof Plans to Sum Series (TW, AN, AB), pp. 325–339.
CAV-1992-Bradfield #model checking #proving: A Proof Assistant for Symbolic Model-Checking (JCB), pp. 316–329.
CSL-1992-ArtemovS #logic #proving: The Basic Logic of Proofs (SNA, TS), pp. 14–28.
CSL-1992-BaazZ #algorithm #proving: Algorithmic Structuring of Cut-free Proofs (MB, RZ), pp. 29–42.
JICSLP-1992-FerrandD #correctness #logic programming #proving #source code: Proof Method of Partial Correctness and Weak Completeness for Normal Logic Programs (GF, PD), pp. 161–174.
JICSLP-1992-GrogerP #automation #logic programming #proving #recursion #source code #termination: Handling of Mutual Recursion in Automatic Termination Proofs for Logic Programs (GG, LP), pp. 336–350.
JICSLP-1992-Wiggins #development #logic programming #proving #source code #synthesis: Synthesis and Transformation of Logic Programs in the Whelk Proof Development System (GAW), pp. 351–365.
LICS-1992-Clote #constant #proving: Cutting Planes and constant depth Frege proofs (PC), pp. 296–307.
DAC-1991-BuschV #design #hardware: Proof-Aided Design of Verified Hardware (HB, GV), pp. 391–396.
STOC-1991-CoffmanG #proving #scheduling: Proof of the 4/3 Conjecture for Preemptive vs. Nonpreemptive Two-Processor Scheduling (EGCJ, MRG), pp. 241–248.
VDME-1991-1-Arthan #on the #proving #specification: On Formal Specification of a Proof Tool (RDA), pp. 356–370.
FPCA-1991-Mairson #parametricity #proving: Outline of a Proof Theory of Parametricity (HGM), pp. 313–327.
LOPSTR-1991-WigginsBKH #induction #logic programming #proving #source code #synthesis: Synthesis and Transfomation of Logic Programs from Constructive, Inductive Proof (GAW, AB, IK, JH), pp. 27–45.
POPL-1991-HenzingerMP #proving #realtime: Temporal Proof Methodologies for Real-time Systems (TAH, ZM, AP), pp. 353–366.
CAV-1991-BevierS #kernel #proving #specification: Mechanically Checked Proofs of Kernel Specification (WRB, JFSA), pp. 70–82.
CAV-1991-MaoM #automation #equivalence #finite #proving #state machine: An Automated Proof Technique for Finite-State Machine Equivalence (WM, GJM), pp. 233–243.
CAV-1991-MauwV #proving: A Proof Assistant for PSF (SM, GJV), pp. 158–168.
CAV-1991-Nesi #higher-order #induction #logic #process #proving #specification: Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic (MN), pp. 288–298.
CAV-1991-SchneiderKK #automation #hardware #proving: Automating Most Parts of Hardware Proofs in HOL (KS, RK, TK), pp. 365–375.
CSL-1991-BeierleB #correctness #proving: Correctness Proof For the WAM with Types (CB, EB), pp. 15–34.
CSL-1991-Goerdt #bound #proving: The Cutting Plane Proof System with Bounded Degree of Falsity (AG), pp. 119–133.
CSL-1991-Schmerl #proving #source code: A Cut-Elimination Procedure Designed for Evaluating Proofs as Programs (URS), pp. 316–325.
CSL-1991-Schwichtenberg #proving: Minimal from Classical Proofs (HS), pp. 326–328.
ICLP-1991-VerschaetseS #logic programming #proving #source code #termination #using: Deriving Termination Proofs for Logic Programs, Using Abstract Procedures (KV, DDS), pp. 301–315.
ISLP-1991-Fribourg #automation #generative #induction #proving: Automatic Generation of Simplification Lemmas for Inductive Proofs (LF), pp. 103–116.
ISLP-1991-HarlandP #linear #logic programming: The Uniform Proof-Theoretic Foundation of Linear Logic Programming (JH, DJP), pp. 304–318.
ISLP-1991-Nakayama #principle #program transformation #proving: Program Transformation under the Principle of Proof as Program (HN), pp. 626–640.
ISLP-1991-Plumer #automation #prolog #proving #source code #termination: Automatic Termination Proofs for Prolog Programs Operating on Nonground Terms (LP), pp. 503–517.
LICS-1991-Boer #composition #process #proving: A Compositional Proof System for Dynamic Process Creation (FSdB), pp. 399–405.
LICS-1991-BonetB #deduction #on the #proving: On the Deduction Rule and the Number of Proof Lines (MLB, SRB), pp. 286–297.
LICS-1991-Hungar #bound #complexity #hoare #proving: Complexity Bounds of Hoare-style Proof Systems (HH), pp. 120–126.
LICS-1991-Murthy #evaluation #proving #semantics: An Evaluation Semantics for Classical Proofs (CRM), pp. 96–107.
RTA-1991-AgarwalMKN #proving: The Tecton Proof System (RA, DRM, DK, XN), pp. 442–444.
RTA-1991-DrewesL #incremental #proving #termination: Incremental Termination Proofs and the Length of Derivations (FD, CL), pp. 49–61.
RTA-1991-Hofbauer #bound #proving #term rewriting #termination: Time Bounded Rewrite Systems and Termination Proofs by Generalized Embedding (DH), pp. 62–73.
RTA-1991-Kirchner #proving #specification: Proofs in Parameterized Specification (HK), pp. 174–187.
DAC-1990-NiermannCP #fault #memory management #named #performance #proving: Proofs: A Fast, Memory Efficient Sequential Circuit Fault Simulator (TMN, WTC, JHP), pp. 535–540.
ICALP-1990-Boer #object-oriented #parallel #proving: A Proof System for the Parallel Object-Oriented Language POOL (FSdB), pp. 572–585.
ICALP-1990-GoldreichK #composition #on the #proving: On the Composition of Zero-Knowledge Proof Systems (OG, HK), pp. 268–282.
ICALP-1990-Riecke #call-by #decidability #proving: A Complete and Decidable Proof System for Call-by-Value Equalities (Preliminary Report) (JGR), pp. 20–31.
ML-1990-Kodratoff #abduction #problem #proving #using: Using Abductive Recovery of Failed Proofs for Problem Solving by Analogy (YK), pp. 295–303.
ALP-1990-Hofbauer #multi #order #proving #recursion #termination: Termination Proofs by Multiset Path Orderings Imply Primitive Recursive Derivation Lengths (DH), pp. 347–358.
POPL-1990-AspertiFG #proving: Implicative Formulae in the “Proofs as Computations” Analogy (AA, GLF, RG), pp. 59–71.
CADE-1990-AltucherP #category theory #proving: A Mechanically Assisted Constructive Proof in Category Theory (JAA, PP), pp. 500–513.
CADE-1990-BundyHSI #induction #proving: Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs (AB, FvH, AS, AI), pp. 132–146.
CADE-1990-EichenlaubEHKP #proving: The Romulus Proof Checker (CE, BE, JH, CK, GP), pp. 651–652.
CADE-1990-FarmerGT #interactive #named #proving: IMPS: An Interactive Mathematical Proof System (WMF, JDG, FJT), pp. 653–654.
CADE-1990-Hutter #induction #proving: Guiding Induction Proofs (DH), pp. 147–161.
CADE-1990-NieP #proving #semantics: A Complete Semantic Back Chaining Proof System (XN, DAP), pp. 16–27.
CADE-1990-Pierce #proving #towards: Toward Mechanical Methods for Streamlining Proofs (WP), pp. 351–365.
CADE-1990-PymW #first-order: Investigations into Proof-Search in a System of First-Order Dependent Function Types (DJP, LAW), pp. 236–250.
CAV-1990-BuyM #liveness #proving: A Proof Lattice-Based Technique for Analyzing Liveness of Resource Controllers (UAB, RM), pp. 292–301.
CLP-1990-Fribourg90 #execution #induction #logic programming #prolog #proving #source code: Extracting Logic Programs from Proofs that Use Extended Prolog Execution and Induction (LF), pp. 685–699.
CLP-1990-Plumer90 #logic programming #proving #source code #termination: Termination Proofs for Logic Programs Based on Predicate Inequalities (LP), pp. 634–648.
CLP-1990-SawamuraMYO90 #approach #logic #logic programming #proving #specification: A Logic Programming Approach to Specifying Logics and Constructing Proofs (HS, TM, KY, KO), pp. 405–424.
CSL-1990-Gabbay #algorithm #proving: Algorithmic Proof with Diminishing Resources, Part 1 (DMG), pp. 156–173.
CSL-1990-Goerdt #proving: Cuting Plane Versus Frege Proof Systems (AG), pp. 174–194.
CSL-1990-Hahnle #logic #multi #performance #proving #towards: Towards an Efficient Tableau Proof Procedure for Multiple-Valued Logics (RH), pp. 248–260.
CSL-1990-HertrampfW #bound #fault #interactive #proving: Interactive Proof Systems: Provers, Rounds, and Error Bounds (UH, KWW), pp. 261–273.
LICS-1990-AllenCHA #proving #semantics: The Semantics of Reflected Proof (SFA, RLC, DJH, WEA), pp. 95–105.
LICS-1990-CleavelandS #proving #specification #using: When is “Partial” Adequate? A Logic-Based Proof Technique Using Partial Specifications (RC, BS), pp. 440–449.
LICS-1990-MurthyR #proving: A Constructive Proof of Higman’s Lemma (CRM, JRR), pp. 257–267.
LICS-1990-Nipkow #equation #proving: Proof Transformations for Equational Theories (TN), pp. 278–288.
NACLP-1990-Spencer #proving: Avoiding Duplicate Proofs (BS), pp. 569–584.
PODS-1989-RamakrishnanSUV #theorem: Proof-Tree Transformation Theorems and Their Applications (RR, YS, JDU, MYV), pp. 172–181.
STOC-1989-Birget #proving: Proof of a Conjecture of R. Kannan (JCB), pp. 445–453.
FPCA-1989-Takayama #performance #proving #source code: Extended Projection — New Method to Extract Efficient Programs from Constructive Proofs (YT), pp. 299–312.
POPL-1989-Paulin-Mohring #calculus #proving #source code: Extracting Fω’s Programs from Proofs in the Calculus of Constructions (CPM), pp. 89–104.
CSL-1989-Ohlbach #first-order #logic #multi #proving: New Ways for Developing Proof Theories for First-Order Multi Modal Logics (HJO), pp. 271–308.
CSL-1989-Stark #proving: A Direct Proof for the Completeness of SLD-Resolution (RFS), pp. 382–383.
LICS-1989-GaifmanS #logic programming #proving #semantics #source code: Proof Theory and Semantics of Logic Programs (HG, EYS), pp. 50–62.
RTA-1989-Bachmair #normalisation #proving: Proof Normalization for Resolution and Paramodulation (LB), pp. 15–28.
RTA-1989-Comon #induction #proving #specification: Inductive Proofs by Specification Transformation (HC), pp. 76–91.
RTA-1989-HofbauerL #proving #termination: Termination Proofs and the Length of Derivations (Preliminary Version) (DH, CL), pp. 167–177.
ESOP-1988-Parigot #higher-order #programming #proving #type system: Programming with Proofs: A Second Order Type Theory (MP), pp. 145–159.
ESOP-1988-Takayama #analysis #compilation #named #proving: QPC: QJ-based Proof Compiler — Simple Examples and Analysis (YT), pp. 49–63.
STOC-1988-Ben-OrGKW #how #interactive #multi #proving: Multi-Prover Interactive Proofs: How to Remove Intractability Assumptions (MBO, SG, JK, AW), pp. 113–131.
VDME-1988-ButhB #code generation #correctness #proving #specification #term rewriting #using: Correctness Proofs for Meta IV Written Code Generator Specification using Term Rewriting (BB, KHB), pp. 406–433.
VDME-1988-Milne #proving: Proof Rules for VDM Statements (RM), pp. 318–336.
ALP-1988-Kucherov #algorithm #induction #proving #testing: A New Quasi-Reducibility Testing Algorithm and its Application to Proofs by Induction (GK), pp. 204–213.
CADE-1988-BrockCP #proving #reasoning: Analogical Reasoning and Proof Discovery (BB, SC, WP), pp. 454–468.
CADE-1988-Bundy #induction #proving: The Use of Explicit Plans to Guide Inductive Proofs (AB), pp. 111–120.
CADE-1988-DuchierM #development #interactive #named #proving: LOGICALC: An Environment for Interactive Proof Development (DD, DVM), pp. 121–130.
CADE-1988-MarcusR #automation #implementation #proving: Two Automated Methods in Implementation Proofs (LM, TR), pp. 622–642.
CADE-1988-Simon #natural language #proving: Checking Natural Language Proofs (DS), pp. 141–150.
CADE-1988-Walther #algorithm #automation #bound #proving #termination: Argument-Bounded Algorithms as a Basis for Automated Termination Proofs (CW), pp. 602–621.
CSL-1988-Plumer #automation #prolog #proving #source code #termination: Predicate Inequalities as a Basis for Automated Termination Proofs for Prolog Programs (LP), pp. 254–271.
JICSCP-1988-BruffaertsH88 #prolog #proving: Proof Trees for Negation as Failure: Yet Another Prolog Meta-Interpreter (AB, EH), pp. 343–358.
LICS-1988-Bachmair #consistency #equation #proving: Proof by Consistency in Equational Theories (LB), pp. 228–233.
LICS-1988-DershowitzO #term rewriting: Proof-Theoretic Techniques for Term Rewriting Theory (ND, MO), pp. 104–111.
LICS-1988-Winskel #composition #petri net #proving: A Category of Labelled Petri Nets and Compositional Proof System (Extended Abstract) (GW), pp. 142–154.
STOC-1987-FeigeFS #proving: Zero Knowledge Proofs of Identity (UF, AF, AS), pp. 210–217.
VDME-1987-Jones87a #proving: VDM Proof Obligations and their Justification (CBJ), pp. 260–286.
POPL-1987-WidomGS #network #proving: Completeness and Incompleteness of Trace-Based Network Proof Systems (JW, DG, FBS), pp. 27–38.
ICLP-1987-Vieille87 #proving: A Database-Complete Proof Procedure Based on SLD-Resolution (LV), pp. 74–103.
LICS-1987-Abadi #power of #proving: The Power of Temporal Proofs (MA), pp. 123–130.
LICS-1987-MillerNS #proving: Hereditary Harrop Formulas and Uniform Proof Systems (DM, GN, AS), pp. 98–105.
SLP-1987-Takayama87 #compilation #prolog #proving #source code: Writing Programs as QJ Proof and Compiling into Prolog Programs (YT), pp. 278–287.
ESOP-1986-Kaplan #algebra #nondeterminism #proving: Rewriting with a Nondeterministic Choice Operator: From Algebra to Proofs (SK), pp. 351–374.
STOC-1986-GoldwasserS #interactive #proving: Private Coins versus Public Coins in Interactive Proof Systems (SG, MS), pp. 59–68.
CADE-1986-Huet #proving: Mechanizing Constructive Proofs (Abstract) (GPH), p. 403.
CADE-1986-KapurNZ #induction #proving #testing #using: Proof by Induction Using Test Sets (DK, PN, HZ), pp. 99–117.
CADE-1986-OppacherS #deduction #heuristic #proving: Controlling Deduction with Proof Condensation and Heuristics (FO, ES), pp. 384–393.
CADE-1986-Wang #named #proving #similarity: ECR: An Equality Conditional Resolution Proof Procedure (TCW), pp. 254–271.
LICS-1986-BachmairDH #equation #order #proving: Orderings for Equational Proofs (LB, ND, JH), pp. 346–357.
LICS-1986-Brookes #concurrent #correctness #csp #proving #semantics: A Semantically Based Proof System for Partial Correctness and Deadlock in CSP (SDB), pp. 58–65.
LICS-1986-Despeyroux #proving #semantics: Proof of Translation in Natural Semantics (JD), pp. 193–205.
LICS-1986-JouannaudK #automation #equation #induction #proving: Automatic Proofs by Induction in Equational Theories Without Constructors (JPJ, EK), pp. 358–366.
SLP-1986-Bledsoe86 #proving: Some Thoughts on Proof Discovery (WWB), pp. 2–10.
STOC-1985-GoldwasserMR #complexity #interactive: The Knowledge Complexity of Interactive Proof-Systems (Extended Abstract) (SG, SM, CR), pp. 291–304.
ICALP-1985-Hansel #proving #theorem: A Simple Proof of the Skolem-Mahler-Lech Theorem (GH), pp. 244–249.
ICALP-1985-Stirling #composition #proving #set: A Complete Compositional Model Proof System for a Subset of CCS (CS), pp. 475–486.
POPL-1985-NguyenGO #network #process #proving: A Model and Temporal Proof System for Networks of Processes (VN, DG, SSO), pp. 121–131.
POPL-1984-RepsA #interactive #proving: Interactive Proof Checking (TWR, BA), pp. 36–45.
ICSE-1984-Chyou #correctness #proving: Structure Charts and Program Correctness Proofs (SCC), pp. 486–498.
CADE-1984-KapurK #proving: A Natural Proof System Based on rewriting Techniques (DK, BK), pp. 53–64.
CADE-1984-Ketonen #named #proving: EKL — A Mathematically Oriented Proof Checker (JK), pp. 65–79.
CADE-1984-Miller #deduction #proving: Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs (DM), pp. 375–393.
CADE-1984-Mulmuley #proving #recursion: The Mechanization of Existence Proofs of Recursive Predicates (KM), pp. 460–475.
CADE-1984-Pfenning #proving: Analytic and Non-analytic Proofs (FP), pp. 394–413.
SLP-1984-AponteFR84 #editing #first-order #proving: Editing First-Order Proofs: Programmed Rules vs Derived Rules (MVA, JAF, PR), pp. 92–98.
POPL-1983-MannaP #how #proving: How to Cook a Temporal Proof System for Your Pet Language (ZM, AP), pp. 141–154.
ICALP-1982-Ben-Ari #algorithm #garbage collection #on the fly #proving: On-the-Fly Garbage Collection: New Algorithms Inspired by Program Proofs (MBA), pp. 14–22.
CADE-1982-Caferra #matrix #proving #reduction #validation: Proof by Matrix Reduction as Plan + Validation (RC), pp. 309–325.
VLDB-1981-BorgidaW #modelling #proving #semantics: Data Models and Data Manipulation Languages: Complementary Semantics and Proof Theory (AB, HKTW), pp. 260–271.
ICALP-1981-Pettorossi #order #proving #recursion #term rewriting #termination: Comparing and Putting Together Recursive Path Ordering, Simplification Orderings and Non-Ascending Property for Termination Proofs of Term Rewriting Systems (AP), pp. 432–447.
ICSE-1981-BaerGGR #modelling #protocol #proving #specification: The Two-Step Commitment Protocol: Modeling, Specification and Proof Methodology (JLB, GG, CG, GR), pp. 363–373.
CADE-1980-Andrews #deduction #proving: Transforming Matings into Natural Deduction Proofs (PBA), pp. 281–292.
CADE-1980-EricksonM #proving #scalability #theorem proving: The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs (RWE, DRM), pp. 220–231.
CADE-1980-Gloess #correctness #empirical #parsing #proving #theorem proving: An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions (PYG), pp. 154–169.
CADE-1980-Goad #proving: Proofs as Description of Computation (CG), pp. 39–52.
STOC-1978-Dowd #proving #representation: Propositional Representation of Arithmetic Proofs (Preliminary Version) (MD), pp. 246–252.
POPL-1978-German #automation #fault #proving #runtime: Automating Proofs of the Absence of Common Runtime Errors (SMG), pp. 105–118.
POPL-1978-GordonMMNW #interactive #metalanguage #proving: A Metalanguage for Interactive Proof in LCF (MJCG, RM, LM, MCN, CPW), pp. 119–130.
STOC-1977-Hartmanis #complexity #proving: Relations Between Diagonalization, Proof Systems, and Complexity Gaps (Preliminary Version) (JH), pp. 223–227.
ICALP-1977-AptB #pascal #proving #semantics: Semantics and Proof Theory of Pascal Procedures (KRA, JWdB), pp. 30–44.
POPL-1977-DeMilloLP #process #proving #social #source code #theorem: Social Processes and Proofs of Theorems and Programs (RAD, RJL, AJP), pp. 206–214.
ICALP-1976-Greif #on the #proving #source code: On Proofs of Programs for Synchronization (IG), pp. 494–507.
ICSE-1976-Gries #correctness #proving #source code: An Illustration of Current Ideas on the Derivation of Correctness Proofs and Correct Programs (Abstract) (DG), p. 200.
ICSE-1976-NeumannFLR #development #multi #proving #security: Software Development and Proofs of Multi-Level Security (PGN, RJF, KNL, LR), pp. 421–428.
STOC-1975-Cook #calculus #proving: Feasibly Constructive Proofs and the Propositional Calculus (Preliminary Version) (SAC), pp. 83–97.
STOC-1975-RivestV #proving: A Generalization and Proof of the Aanderaa-Rosenberg Conjecture (RLR, JV), pp. 6–11.
STOC-1974-CookR #calculus #on the #proving: On the Lengths of Proofs in the Propositional Calculus (Preliminary Version) (SAC, RAR), pp. 135–148.
ICALP-1972-HitchcockP #induction #proving #termination: Induction Rules and Termination Proofs (PH, DMRP), pp. 225–251.
STOC-1970-Rounds #proving #theorem: Tree-Oriented Proofs of Some Theorems on Context-Free and Indexed Languages (WCR), pp. 109–116.