BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Used together with:
system (117)
program (116)
logic (95)
base (55)
abstract (48)

Stem proof$ (all stems)

896 papers:

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

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