BibSLEIGH — proving tag

proving

proving

Tag #proving

1503 papers:

POPL-2020-AschieriG #concurrent #functional #linear #logic #parallel #source code: Par means parallel: multiplicative linear logic proofs as concurrent functional programs (FA, FAG), p. 28.
POPL-2020-BartheHYYZ #quantum #relational #source code: Relational proofs for quantum programs (GB, JH, MY, NY, LZ), p. 29.
POPL-2020-FarzanV #reduction #safety: Reductions for safety proofs (AF, AV), p. 28.
POPL-2020-WangFCDX #probability #random #source code #termination: Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time (PW, HF0, KC, YD, MX), p. 30.
CSL-2020-Buss0K #branch #complexity #nondeterminism #source code: Proof Complexity of Systems of (Non-Deterministic) Decision Trees and Branching Programs (SB, AD0, AK), p. 17.
CSL-2020-Tzameret #bound: From Classical Proof Theory to P versus NP: a Guide to Bounded Theories (Invited Talk) (IT), p. 2.
SANER-2019-YukizawaTT #case study #exclamation #social: Please Help! A Preliminary Study on the Effect of Social Proof and Legitimization of Paltry Contributions in Donations to OSS (UY, MT, AT), pp. 609–613.
FM-2019-MarmsolerB #architecture #modelling #named: APML: An Architecture Proof Modeling Language (DM, GB), pp. 611–630.
FSCD-2019-Diaz-CaroD #identification #logic #normalisation: Proof Normalisation in a Logic Identifying Isomorphic Propositions (ADC, GD), p. 23.
FSCD-2019-HeijltjesHS #first-order #linear #logic: Proof Nets for First-Order Additive Linear Logic (WH, DJDH, LS), p. 22.
FSCD-2019-Horne #linear #logic #probability: The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic (RH), p. 16.
IFM-2019-KringsL #constraints #interactive #theorem proving: Embedding SMT-LIB into B for Interactive Proof and Constraint Solving (SK, ML), pp. 265–283.
ICFP-2019-SozeauM #coq #equation #functional #programming: Equations reloaded: high-level dependently-typed functional programming and proving in Coq (MS, CM), p. 29.
ICML-2019-BansalLRSW #higher-order #logic #machine learning #named #theorem proving: HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving (KB, SML, MNR, CS, SW), pp. 454–463.
ICML-2019-YangD #learning #theorem: Learning to Prove Theorems via Interacting with Proof Assistants (KY, JD), pp. 6984–6994.
PADL-2019-Tarau #combinator #framework #testing #theorem proving: A Combinatorial Testing Framework for Intuitionistic Propositional Theorem Provers (PT), pp. 115–132.
PEPM-2019-Asai #call-by #termination: Extracting a call-by-name partial evaluator from a proof of termination (KA), pp. 61–67.
PLDI-2019-WangDWKZ #difference #execution #privacy: Proving differential privacy with shadow execution (YW, ZD, GW, DK, DZ), pp. 655–669.
PPDP-2019-Blanco0M #re-engineering #testing: Property-Based Testing via Proof Reconstruction (RB, DM0, AM), p. 13.
PPDP-2019-Kikuchi0S #induction #program transformation #term rewriting #theorem proving: Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation (KK, TA0, IS), p. 14.
ESOP-2019-BasoldKL #horn clause #induction #recursion: Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses (HB, EK, YL), pp. 783–813.
ESOP-2019-MartinezADGHHNP #automation #metaprogramming #smt: Meta-F* : Proof Automation with SMT, Tactics, and Metaprograms (GM, DA, VD, NG, CH, CH, MN, ZP, CPC, JP, TR, AR, NS), pp. 30–59.
CADE-2019-KohlM: Composing Proof Terms (CK, AM), pp. 337–353.
CADE-2019-LiT #automation #protocol #security #theorem proving #verification: Combining ProVerif and Automated Theorem Provers for Security Protocol Verification (DLL, AT), pp. 354–365.
CADE-2019-NiemetzPRZBT #independence #smt #towards: Towards Bit-Width-Independent Proofs in SMT Solvers (AN, MP, AR, YZ, CWB, CT), pp. 366–384.
CADE-2019-RegerV #induction: Induction in Saturation-Based Proof Search (GR, AV), pp. 477–494.
CAV-2019-DavisHK #fault #formal method #multi #protocol #using: When Human Intuition Fails: Using Formal Methods to Find an Error in the “Proof” of a Multi-agent Protocol (JAD, LRH, DBK), pp. 366–375.
CAV-2019-HuBCDR #synthesis: Proving Unrealizability for Syntax-Guided Synthesis (QH, JB, JC, LD, TWR), pp. 335–352.
CAV-2019-GaoKDRSAK #induction: Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems (SG, JK, JVD, NR, ASL, NA, SK), pp. 137–154.
ICTSS-2019-SachtlebenHH0 #adaptation #algorithm: A Mechanised Proof of an Adaptive State Counting Algorithm (RS, RMH, WlH, JP0), pp. 176–193.
TAP-2019-HuraultQ #algorithm #process: Proving a Non-blocking Algorithm for Process Renaming with TLA ^+ + (AH, PQ), pp. 147–166.
TAP-2019-RoblesKPRG #specification #testing: Tame Your Annotations with MetAcsl: Specifying, Testing and Proving High-Level Properties (VR, NK, VP, LR, PLG), pp. 167–185.
VMCAI-2019-PreoteasaDT #diagrams: Mechanically Proving Determinacy of Hierarchical Block Diagram Translations (VP, ID, ST), pp. 577–600.
FM-2018-Boralv #automation #design #using: Interlocking Design Automation Using Prover Trident (AB), pp. 653–656.
FM-2018-Cohen #object-oriented #security: Object-Oriented Security Proofs (EC), pp. 671–674.
FSCD-2018-BellinH #linear #logic: Proof Nets for Bi-Intuitionistic Linear Logic (GB, WH), p. 18.
FSCD-2018-KohlM #named: ProTeM: A Proof Term Manipulator (System Description) (CK, AM), p. 8.
FSCD-2018-Nguyen: Unique perfect matchings and proof nets (LTDN), p. 20.
FSCD-2018-Vignudelli #equivalence #higher-order #probability: Proof Techniques for Program Equivalence in Probabilistic Higher-Order Languages (Invited Talk) (VV), p. 2.
SEFM-2018-DuboisGPC #interactive #protocol #theorem proving #using: Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem Prover (CD, OG, JP, MC), pp. 239–253.
SEFM-2018-SchellhornWTKW #case study: FastLane Is Opaque - a Case Study in Mechanized Proofs of Opacity (GS, MW, OT, JK, HW), pp. 105–120.
Haskell-2018-Noonan #functional: Ghosts of departed proofs (functional pearl) (MN), pp. 119–131.
Haskell-2018-VazouBKHH #equation #functional #haskell #reasoning #theorem proving: Theorem proving for all: equational reasoning in liquid Haskell (functional pearl) (NV, JB, RK, DVH, GH), pp. 132–144.
ICFP-2018-AllaisA0MM #semantics: A type and scope safe universe of syntaxes with binding: their semantics and proofs (GA, RA, JC0, CM, JM), p. 30.
ICFP-2018-KeidelPE #composition: Compositional soundness proofs of abstract interpreters (SK, CBP, SE), p. 26.
ICFP-2018-KrebbersJ0TKTCD #framework #interactive #logic #named: MoSeL: a general, extensible modal framework for interactive proofs in separation logic (RK, JHJ, RJ0, JT, JOK, AT, AC, DD), p. 30.
LOPSTR-2018-Lucas #first-order #satisfiability: Proving Program Properties as First-Order Satisfiability (SL), pp. 3–21.
POPL-2018-AlbarghouthiH #difference #privacy: Synthesizing coupling proofs of differential privacy (AA, JH), p. 30.
POPL-2018-BartheEGHS #probability #source code: Proving expected sensitivity of probabilistic programs (GB, TE, BG, JH, PYS), p. 29.
POPL-2018-Lee0A #automation #correctness #implementation #on the: On automatically proving the correctness of math.h implementations (WL0, RS0, AA), p. 32.
POPL-2018-LodingMP #quantifier: Foundations for natural proofs and quantifier instantiation (CL, PM, LP), p. 30.
POPL-2018-McIverMKK #termination: A new proof rule for almost-sure termination (AM, CM, BLK, JPK), p. 28.
POPL-2018-SergeyWT #distributed #programming #protocol: Programming and proving with distributed protocols (IS, JRW, ZT), p. 30.
POPL-2018-TimanySKB #encapsulation #logic #monad: A logical relation for monadic encapsulation of state: proving contextual equivalences in the presence of runST (AT, LS, MKJ, LB), p. 28.
PPDP-2018-GreweEPM #automation #framework #theorem proving: System Description: An Infrastructure for Combining Domain Knowledge with Automated Theorem Provers (SG, SE, AP, MM), p. 10.
PPDP-2018-NadathurW #morphism #polymorphism: Schematic Polymorphism in the Abella Proof Assistant (GN, YW), p. 13.
SAS-2018-PrabhuMV #behaviour #learning #safety: Efficiently Learning Safety Proofs from Appearance as well as Behaviours (SP, KM, RV), pp. 326–343.
SAS-2018-Zuleger #abstraction #induction #invariant #termination: Inductive Termination Proofs with Transition Invariants and Their Relationship to the Size-Change Abstraction (FZ), pp. 423–444.
ASE-2018-NagashimaH #higher-order #named #recommendation: PaMpeR: proof method recommendation system for Isabelle/HOL (YN, YH), pp. 362–372.
ESEC-FSE-2018-HellendoornDA #on the: On the naturalness of proofs (VJH, PTD, MAA), pp. 724–728.
CAV-2018-AlbarghouthiH #constraints #synthesis: Constraint-Based Synthesis of Coupling Proofs (AA, JH), pp. 327–346.
CAV-2018-ChevalKR: The DEEPSEC Prover (VC, SK, IR), pp. 28–36.
CAV-2018-RobereKG #complexity #smt: The Proof Complexity of SMT Solvers (RR, AK, VG), pp. 275–293.
CSL-2018-ChouquetA #linear #logic #parallel: An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets (JC, LVA), p. 17.
CSL-2018-DasP #algebra: Non-Wellfounded Proof Theory For (Kleene+Action)(Algebras+Lattices) (AD0, DP), p. 18.
CSL-2018-NolletST #fixpoint #linear #logic: Local Validity for Circular Proofs in Linear Logic with Fixed Points (RN, AS, CT), p. 23.
IJCAR-2018-AcclavioS #combinator: From Syntactic Proofs to Combinatorial Proofs (MA, LS), pp. 481–497.
IJCAR-2018-CiobacaL #approach #induction #reachability #term rewriting: A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems (SC, DL), pp. 295–311.
IJCAR-2018-LettmannP #calculus: A Tableaux Calculus for Reducing Proof Size (MPL, NP), pp. 64–80.
IJCAR-2018-MelquiondR #algorithm #framework #why: A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms (GM, RRH), pp. 178–193.
IJCAR-2018-SchlichtkrullBT #formal method #order: Formalizing Bachmair and Ganzinger's Ordered Resolution Prover (AS, JCB, DT, UW), pp. 89–107.
IJCAR-2018-SteenB #higher-order: The Higher-Order Prover Leo-III (AS, CB), pp. 108–116.
TAP-2018-BruckerH #formal method #standard #web: Formalizing (Web) Standards - An Application of Test and Proof (ADB, MH), pp. 159–166.
TAP-2018-LeCSW #verification: Verification Coverage for Combining Test and Proof (VHL, LC, JS, VW), pp. 120–138.
VMCAI-2018-ZuckMT #probability #protocol: P^5 : Planner-less Proofs of Probabilistic Parameterized Protocols (LDZ, KLM, JT), pp. 336–357.
DLT-2017-Beier0 #complexity #on the #regular expression: On Regular Expression Proof Complexity (SB, MH0), pp. 83–95.
FSCD-2017-0001TK #approach #confluence #induction: Improving Rewriting Induction Approach for Proving Ground Confluence (TA0, YT, YK), p. 18.
IFM-2017-ChenF #first-order #verification: Triggerless Happy - Intermediate Verification with a First-Order Prover (YC, CAF), pp. 295–311.
SEFM-2017-BernasconiMSZG #model checking #modelling: From Model Checking to a Temporal Proof for Partial Models (AB0, CM, PS, LDZ, CG), pp. 54–69.
SEFM-2017-Jakobs #analysis: PART_PW : From Partial Analysis Results to a Proof Witness (MCJ), pp. 120–135.
Haskell-2017-VazouLP #coq #haskell #string #verification: A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq (NV, LL, JP), pp. 63–74.
OOPSLA-2017-RapoportKHL: A simple soundness proof for dependent object types (MR, IK, PH, OL), p. 27.
PLDI-2017-AntonopoulosGHK #composition #self: Decomposition instead of self-composition for proving the absence of timing channels (TA, PG, MH0, EK, TT, SW), pp. 362–375.
PLDI-2017-ChuWCS #named #query #semantics #sql: HoTTSQL: proving query rewrites with univalent SQL semantics (SC, KW, AC, DS), pp. 510–524.
POPL-2017-AlglaveC #consistency #modelling: Ogre and Pythia: an invariance proof method for weak consistency models (JA, PC), pp. 3–18.
POPL-2017-AminR: Type soundness proofs with definitional interpreters (NA, TR), pp. 666–679.
POPL-2017-BartheGHS #probability #source code: Coupling proofs are probabilistic product programs (GB, BG, JH, PYS), pp. 161–174.
POPL-2017-KrebbersTB #concurrent #higher-order #interactive #logic: Interactive proofs in higher-order concurrent separation logic (RK, AT, LB), pp. 205–217.
POPL-2017-ZhangK #automation #difference #named #privacy #towards: LightDP: towards automating differential privacy proofs (DZ, DK), pp. 888–901.
ASE-2017-CelikPG #named #scalability #verification: iCoq: regression proof selection for large-scale verification projects (AÇ, KP, MG), pp. 171–182.
ESOP-2017-BlanchetteBL0T #implementation #recursion: Friends with Benefits - Implementing Corecursion in Foundational Proof Assistants (JCB, AB, AL, AP0, DT), pp. 111–140.
ESOP-2017-KhyzhaDGP #partial order #using: Proving Linearizability Using Partial Orders (AK, MD, AG, MJP), pp. 639–667.
CADE-2017-BarbosaBF #fine-grained #scalability: Scalable Fine-Grained Proofs for Formula Processing (HB, JCB, PF), pp. 398–412.
CADE-2017-BlancoCM: Translating Between Implicit and Explicit Versions of Proof (RB, ZC, DM0), pp. 255–273.
CADE-2017-BrockschmidtJT0 #integer #safety #termination: Certifying Safety and Termination Proofs for Integer Transition Systems (MB, SJCJ, RT, AY0), pp. 454–471.
CADE-2017-FarberKU #monte carlo: Monte Carlo Tableau Proof Search (MF0, CK, JU), pp. 563–579.
CADE-2017-GleissK0: Splitting Proofs for Interpolation (BG, LK, MS0), pp. 291–309.
CADE-2017-HeuleKB: Short Proofs Without New Variables (MJHH, BK, AB), pp. 130–147.
CADE-2017-HustadtOD #logic #metric #theorem proving: Theorem Proving for Metric Temporal Logic over the Naturals (UH, AO, CD), pp. 326–343.
CADE-2017-ItegulovSP #theorem proving: Scavenger 0.1: A Theorem Prover Based on Conflict Resolution (DI, JS, BWP), pp. 344–356.
CADE-2017-NagashimaK #generative #higher-order: A Proof Strategy Language and Proof Script Generation for Isabelle/HOL (YN, RK), pp. 528–545.
CADE-2017-TellezB #automation #pointer #source code #verification: Automatically Verifying Temporal Properties of Pointer Programs with Cyclic Proof (GT, JB), pp. 491–508.
CAV-2017-BouajjaniEEM #simulation #using: Proving Linearizability Using Forward Simulations (AB, ME, CE, SOM), pp. 542–563.
CAV-2017-Carbonneaux0RS #analysis #automation #coq: Automated Resource Analysis with Coq Proof Objects (QC, JH0, TWR, ZS), pp. 64–85.
CAV-2017-GasconTCM #component #synthesis: Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis (AG, AT0, BC, UM), pp. 86–103.
CSL-2017-GradelPP: The Model-Theoretic Expressiveness of Propositional Proof Systems (EG, BP, WP), p. 18.
CSL-2017-Kovacs #first-order: First-Order Interpolation and Grey Areas of Proofs (Invited Talk) (LK), p. 1.
CSL-2017-TubellaGR: Removing Cycles from Proofs (AAT, AG, BR), p. 17.
ICST-2017-DarkeCCV #abstraction #bound #model checking #performance #safety #using: Efficient Safety Proofs for Industry-Scale Code Using Abstractions and Bounded Model Checking (PD, BC, AC, RV), pp. 468–475.
TAP-2017-Reger0V #case study #challenge #experience #testing #theorem proving: Testing a Saturation-Based Theorem Prover: Experiences and Challenges (GR, MS0, AV), pp. 152–161.
VMCAI-2017-FrumkinFLPSS #concurrent #fault #reachability: Property Directed Reachability for Proving Absence of Concurrent Modification Errors (AF, YMYF, OL, OP, MS, SS), pp. 209–227.
FM-2016-BeckerCGHHKNSTT #analysis #formal method #modelling #testing: Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor (HB, JMC, JG, UH, YH, CK, KN0, JLS, HT, TT), pp. 69–84.
FM-2016-KhyzhaGP #logic: A Generic Logic for Proving Linearizability (AK, AG, MJP), pp. 426–443.
FM-2016-TaLKC #automation #induction #logic: Automated Mutual Explicit Induction Proof in Separation Logic (QTT, TCL, SCK, WNC), pp. 659–676.
FSCD-2016-0001T #confluence #induction: Ground Confluence Prover based on Rewriting Induction (TA0, YT), p. 12.
FSCD-2016-BarKV #named #online: Globular: An Online Proof Assistant for Higher-Dimensional Rewriting (KB, AK, JV), p. 11.
FSCD-2016-BrenasES #correctness #graph grammar #term rewriting: Proving Correctness of Logically Decorated Graph Rewriting Systems (JHB, RE, MS), p. 15.
FSCD-2016-ChaudhuriMS #composition #logic: Modular Focused Proof Systems for Intuitionistic Modal Logics (KC, SM, LS), p. 18.
FSCD-2016-GuerrieriPF: Computing Connected Proof(-Structure)s From Their Taylor Expansion (GG, LP, LTdF), p. 18.
IFM-2016-SchellhornTW #thread #towards: Towards a Thread-Local Proof Technique for Starvation Freedom (GS, OT, HW), pp. 193–209.
SEFM-2016-ArcainiGR #automation #refinement #smt: SMT-Based Automatic Proof of ASM Model Refinement (PA, AG, ER), pp. 253–269.
SEFM-2016-HauzarMM: Counterexamples from Proof Failures in SPARK (DH, CM, YM), pp. 215–233.
SEFM-2016-HenselGFS #execution #source code #symbolic computation #termination: Proving Termination of Programs with Bitvector Arithmetic by Symbolic Execution (JH, JG, FF, TS), pp. 234–252.
SEFM-2016-ZellerP #consistency #framework #information management #towards: Towards a Proof Framework for Information Systems with Weak Consistency (PZ0, APH), pp. 277–283.
PPDP-2016-NagaoN #induction: Proving inductive validity of constrained inequalities (TN, NN0), pp. 50–61.
ASE-2016-HentschelHB16a #comprehension #debugging #effectiveness #interactive #verification: The interactive verification debugger: effective understanding of interactive proof attempts (MH, RH, RB), pp. 846–851.
FASE-2016-0001K #metric #towards: Towards Formal Proof Metrics (DA0, CK), pp. 325–341.
CAV-2016-DooleyS: Proving Parameterized Systems Safe by Generalizing Clausal Proofs of Small Instances (MD, FS), pp. 292–309.
CSL-2016-BaeldeDS #multi: Infinitary Proof Theory: the Multiplicative Additive Case (DB, AD, AS), p. 17.
IJCAR-2016-NalonHD #multimodal: : A Resolution-Based Prover for Multimodal K (CN, UH, CD), pp. 406–415.
IJCAR-2016-Otten #named: nanoCoP: A Non-clausal Connection Prover (JO), pp. 302–312.
IJCAR-2016-Platzer #cyber-physical #logic: Logic & Proofs for Cyber-Physical Systems (AP), pp. 15–21.
IJCAR-2016-SchulzM #heuristic #performance #theorem proving: Performance of Clause Selection Heuristics for Saturation-Based Theorem Proving (SS0, MM), pp. 330–345.
TAP-2016-DuboisGG #combinator #testing: Tests and Proofs for Enumerative Combinatorics (CD, AG, RG), pp. 57–75.
TAP-2016-PetiotKBGJ #testing: Your Proof Fails? Testing Helps to Find the Reason (GP, NK, BB, AG, JJ), pp. 130–150.
VLDB-2015-PapadopoulosPTT #authentication #pattern matching: Practical Authenticated Pattern Matching with Optimal Proof Size (DP, CP, RT, NT), pp. 750–761.
ICALP-v1-2015-CoudronV #approximate #interactive: Interactive Proofs with Approximately Commuting Provers (MC, TV), pp. 355–366.
ICALP-v1-2015-GoldreichGR #branch #context-free grammar #proximity #source code: Proofs of Proximity for Context-Free Languages and Read-Once Branching Programs — (OG, TG, RDR), pp. 666–677.
ICALP-v2-2015-AisenbergBBCI #principle: Short Proofs of the Kneser-Lovász Coloring Principle (JA, MLB, SB, AC, GI), pp. 44–55.
FM-2015-KroeningLW #automaton #bound #model checking #safety: Proving Safety with Trace Automata and Bounded Model Checking (DK, ML, GW), pp. 325–341.
HOFM-2015-Adams #refactoring: Refactoring Proofs with Tactician (MA), pp. 53–67.
RTA-2015-AvanziniST #certification #complexity #using: Certification of Complexity Proofs using CeTA (MA, CS, RT), pp. 23–39.
RTA-2015-EndrullisZ #automaton #finite: Proving non-termination by finite automata (JE, HZ), pp. 160–176.
SEFM-2015-KringsBL: From Failure to Proof: The ProB Disprover for B and Event-B (SK, JB, ML), pp. 199–214.
TLCA-2015-Bagnol #diagrams #equivalence: MALL Proof Equivalence is Logspace-Complete, via Binary Decision Diagrams (MB), pp. 60–75.
Haskell-2015-Breitner #compilation: Formally proving a compiler transformation safe (JB), pp. 35–46.
ICFP-2015-Blanchette0T #perspective #recursion: Foundational extensible corecursion: a proof assistant perspective (JCB, AP, DT), pp. 192–204.
FDG-2015-Martens #game studies #using: Using Proof Theory to Study Game Mechanics (CM).
ICGT-2015-Bruggink0NZ #graph #graph transformation #termination #using: Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings (HJSB, BK, DN, HZ), pp. 52–68.
CIKM-2015-WangYWH #scalability: Large-Scale Question Answering with Joint Embedding and Proof Tree Decoding (ZW, SY, HW, XH), pp. 1783–1786.
KDD-2015-Pratt #machine learning #predict #protocol: Proof Protocol for a Machine Learning Technique Making Longitudinal Predictions in Dynamic Contexts (KBP), pp. 2049–2058.
Onward-2015-GreweEWM #performance #type system: Type systems for the masses: deriving soundness proofs and efficient checkers (SG, SE, PW, MM), pp. 137–150.
LOPSTR-2015-Miller #logic programming: Proof Checking and Logic Programming (DM0), pp. 3–17.
PLDI-2015-ChuJT #automation #imperative #induction #source code: Automatic induction proofs of data-structures in imperative programs (DHC, JJ, MTT), pp. 457–466.
POPL-2015-DelawarePGC #data type #deduction #named #synthesis: Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant (BD, CPC, JG, AC), pp. 689–700.
POPL-2015-FarzanKP #bound #parallel: Proof Spaces for Unbounded Parallelism (AF, ZK, AP), pp. 407–420.
PPDP-2015-Miller #logic programming: Proof checking and logic programming (DM), p. 18.
ASE-2015-ChenDKSW #interprocedural #termination: Synthesising Interprocedural Bit-Precise Termination Proofs (T) (HYC, CD, DK, PS, BW), pp. 53–64.
ICSE-v2-2015-EtienneMAD #modelling #performance #predict #process #trust: Improving Predictability, Efficiency and Trust of Model-Based Proof Activity (JFÉ, MM, FA, VD), pp. 139–148.
SAC-2015-JakobsW #analysis #data flow #source code: Programs from proofs of predicated dataflow analyses (MCJ, HW), pp. 1729–1736.
DATE-2015-ReichPEB #component #design #flexibility: Silicon proof of the intelligent analog IP design flow for flexible automotive components (TR, HDBP, UE, RB), pp. 403–404.
SOSP-2015-HawblitzelHKLPR #distributed #named: IronFleet: proving practical distributed systems correct (CH, JH, MK, JRL, BP, MLR, STVS, BZ), pp. 1–17.
STOC-2015-DingSS #satisfiability #scalability: Proof of the Satisfiability Conjecture for Large k (JD, AS, NS), pp. 59–68.
TACAS-2015-CiniF #ltl #runtime #verification: An LTL Proof System for Runtime Verification (CC, AF), pp. 581–595.
TACAS-2015-MolnarDVB #incremental #induction #ltl #model checking: Saturation-Based Incremental LTL Model Checking with Inductive Proofs (VM, DD, AV, TB), pp. 643–657.
CADE-2015-BackemanR #bound #theorem proving: Theorem Proving with Bounded Rigid E-Unification (PB, PR), pp. 572–587.
CADE-2015-Baumgartner #named #theorem proving: SMTtoTPTP — A Converter for Theorem Proving Formats (PB), pp. 285–294.
CADE-2015-BaumgartnerBW #named #theorem proving: Beagle — A Hierarchic Superposition Theorem Prover (PB, JB, UW), pp. 367–377.
CADE-2015-FultonMQVP #axiom #hybrid #theorem proving: KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems (NF, SM, JDQ, MV, AP), pp. 527–538.
CADE-2015-GorznyP #first-order #towards: Towards the Compression of First-Order Resolution Proofs by Lowering Unit Clauses (JG, BWP), pp. 356–366.
CADE-2015-GransdenWR #automaton #named #using: SEPIA: Search for Proofs Using Inferred Automata (TG, NW, RR), pp. 246–255.
CADE-2015-HeuleHW #symmetry: Expressing Symmetry Breaking in DRAT Proofs (MH, WAHJ, NW), pp. 591–606.
CADE-2015-HouGT #automation #logic #theorem proving: Automated Theorem Proving for Assertions in Separation Logic with All Connectives (ZH, RG, AT), pp. 501–516.
CADE-2015-KissingerZ #diagrams #named #reasoning: Quantomatic: A Proof Assistant for Diagrammatic Reasoning (AK, VZ), pp. 326–336.
CADE-2015-MaricJM #correctness #higher-order #using: Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 (FM, PJ, MM), pp. 256–271.
CADE-2015-MouraKADR #agile #theorem proving: The Lean Theorem Prover (LMdM, SK, JA, FvD, JvR), pp. 378–388.
CADE-2015-PientkaC #induction #programming: Inductive Beluga: Programming Proofs (BP, AC), pp. 272–281.
CADE-2015-RegerTV: Cooperating Proof Attempts (GR, DT, AV), pp. 339–355.
CAV-2015-KarbyshevBIRS #invariant: Property-Directed Inference of Universal Invariants or Proving Their Absence (AK, NB, SI, NR, SS), pp. 583–602.
CAV-2015-ZhuPJ #named #smt: Poling: SMT Aided Linearizability Proofs (HZ, GP, SJ), pp. 3–19.
CSL-2015-SchubertDB #automaton: Automata Theoretic Account of Proof Search (AS, WD, HPB), pp. 128–143.
ICLP-J-2015-AngelisFPP #correctness #horn clause #imperative #source code: Proving correctness of imperative programs by linearizing constrained Horn clauses (EDA, FF, AP, MP), pp. 635–650.
ISSTA-2015-AquinoBCDP #constraints #program analysis #reuse: Reusing constraint proofs in program analysis (AA, FAB, MC, GD, MP), pp. 305–315.
LICS-2015-BaazLR #complexity: A Note on the Complexity of Classical and Intuitionistic Proofs (MB, AL, GR), pp. 657–666.
LICS-2015-HeijltjesH #bound #complexity #logic #petri net: Complexity Bounds for Sum-Product Logic via Additive Proof Nets and Petri Nets (WH, DJDH), pp. 80–91.
VMCAI-2015-ChristakisG #composition #image #memory management #parsing #safety #testing #using: Proving Memory Safety of the ANI Windows Image Parser Using Compositional Exhaustive Testing (MC, PG), pp. 373–392.
VMCAI-2015-GhorbalSP #algebra #difference #set: A Hierarchy of Proof Rules for Checking Differential Invariance of Algebraic Sets (KG, AS, AP), pp. 431–448.
VMCAI-2015-UrbanM #abstract interpretation: Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation (CU, AM), pp. 190–208.
PODS-2014-BenediktCT #generative #low cost: Generating low-cost plans from proofs (MB, BtC, ET), pp. 200–211.
AFL-2014-Valmari #string: Character Strings and Gödel’s Incompleteness Proof (AV), pp. 355–369.
ICALP-v1-2014-Ben-SassonRTW #algorithm: Sampling-Based Proofs of Almost-Periodicity Results and Algorithmic Applications (EBS, NRZ, MT, JW), pp. 955–966.
ICALP-v1-2014-OstrovskyPV #on the: On Input Indistinguishable Proof Systems (RO, GP, IV), pp. 895–906.
ICALP-v1-2014-TalwarW: Balanced Allocations: A Simple Proof for the Heavily Loaded Case (KT, UW), pp. 979–990.
FM-2014-DenmanM #automation: Automated Real Proving in PVS via MetiTarski (WD, CAM), pp. 194–199.
FM-2014-FreitasW #formal method: Proof Patterns for Formal Methods (LF, IW), pp. 279–295.
FM-2014-Klein: Proof Engineering Considered Essential (GK), pp. 16–21.
FM-2014-LeinoM #automation #induction #verification: Co-induction Simply — Automatic Co-inductive Proofs in a Program Verifier (KRML, MM), pp. 382–398.
HOFM-2014-BeckertGB #evaluation #interactive #theorem proving #usability #using: A Usability Evaluation of Interactive Theorem Provers Using Focus Groups (BB, SG, FB), pp. 3–19.
IFM-2014-ChaudhariD #automation #theorem proving: Automated Theorem Prover Assisted Program Calculations (DLC, OPD), pp. 205–220.
IFM-2014-ErikssonPB #invariant #programming: Proofs and Refutations in Invariant-Based Programming (JE, MP, RJB), pp. 189–204.
IFM-2014-TofanSR #composition #multi: A Compositional Proof Method for Linearizability Applied to a Wait-Free Multiset (BT, GS, WR), pp. 357–372.
RTA-TLCA-2014-AotoTU #confluence #diagrams #term rewriting: Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams (TA, YT, KU), pp. 46–60.
RTA-TLCA-2014-Czajka #confluence #induction #λ-calculus: A Coinductive Confluence Proof for Infinitary λ-Calculus (LC), pp. 164–178.
RTA-TLCA-2014-LombardiRV: Proof Terms for Infinitary Rewriting (CL, AR, RdV), pp. 303–318.
RTA-TLCA-2014-Maieli: Construction of Retractile Proof Structures (RM), pp. 319–333.
RTA-TLCA-2014-SternagelT #algebra #certification #complexity #formal method #termination: Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs (CS, RT), pp. 441–455.
SEFM-2014-Leroy #code generation #tool support #verification: Formal Proofs of Code Generation and Verification Tools (XL), pp. 1–4.
FLOPS-2014-Bahr #compilation #correctness #graph #using: Proving Correctness of Compilers Using Structured Graphs (PB), pp. 221–237.
HCI-AIMT-2014-RederMFK #arduino #concept #human-computer #interactive #interface: Neural Interface Emotiv EPOC and Arduino: Brain-Computer Interaction in a Proof of Concept (EER, ARdQM, VRTF, FK), pp. 612–623.
LCT-NLE-2014-PaisT #deduction #first-order #logic #novel: Novel Didactic Proof Assistant for First-Order Logic Natural Deduction (JP, AT), pp. 441–451.
SPLC-2014-ThumMBHRS #model checking #product line #theorem proving: Potential synergies of theorem proving and model checking for software product lines (TT, JM, FB, MH, AvR, GS), pp. 177–186.
OOPSLA-2014-Desai0M #reduction #source code #using: Natural proofs for asynchronous programs using almost-synchronous reductions (AD, PG, PM), pp. 709–725.
PLDI-2014-PekQM #c #data type #logic #using: Natural proofs for data structure manipulation in C using separation logic (EP, XQ, PM), p. 46.
PLDI-2014-RickettsRJTL #automation: Automating formal proofs for reactive systems (DR, VR, DJ, ZT, SL), p. 47.
POPL-2014-CasinghinoSW #source code: Combining proofs and programs in a dependently typed language (CC, VS, SW), pp. 33–46.
POPL-2014-ChaudhuriCS #synthesis #using: Bridging boolean and quantitative synthesis using smoothed proof search (SC, MC, ASL), pp. 207–220.
POPL-2014-FarzanKP: Proofs that count (AF, ZK, AP), pp. 151–164.
POPL-2014-HouCGT #logic: Proof search for propositional abstract separation logics via labelled sequents (ZH, RC, RG, AT), pp. 465–476.
POPL-2014-LeeP #logic: A proof system for separation logic with magic wand (WL, SP), pp. 477–490.
PPDP-2014-AotoS #induction #theorem: Decision Procedures for Proving Inductive Theorems without Induction (TA, SS), pp. 237–248.
PPDP-2014-Ilik #continuation #normalisation #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.
PPDP-2014-LucasM #declarative #logic #source code #termination: Proving Operational Termination of Declarative Programs in General Logics (SL, JM), pp. 111–122.
PPDP-2014-MehnerSSV #functional #parametricity #theorem: Parametricity and Proving Free Theorems for Functional-Logic Languages (SM, DS, LS, JV), pp. 19–30.
SAS-2014-UrbanM #abstract domain #termination: A Decision Tree Abstract Domain for Proving Conditional Termination (CU, AM), pp. 302–318.
DATE-2014-Jin #evaluation #security #tool support #trust: EDA tools trust evaluation through security property proofs (YJ), pp. 1–4.
ESOP-2014-BrainDKS #generative #source code: Model and Proof Generation for Heap-Manipulating Programs (MB, CD, DK, PS), pp. 432–452.
ESOP-2014-YoshimizuHFL #higher-order #metric #quantum: Measurements in Proof Nets as Higher-Order Quantum Circuits (AY, IH, CF, UDL), pp. 371–391.
STOC-2014-KalaiRR #how #power of: How to delegate computations: the power of no-signaling proofs (YTK, RR, RDR), pp. 485–494.
TACAS-2014-ChenCFNO #safety: Proving Nontermination via Safety (HYC, BC, CF, KN, PWO), pp. 156–171.
TACAS-2014-Cheval #algorithm #equivalence #named: APTE: An Algorithm for Proving Trace Equivalence (VC), pp. 587–592.
WRLA-2014-LucasM14a #2d #dependence #termination: 2D Dependency Pairs for Proving Operational Termination of CTRSs (SL, JM), pp. 195–212.
CAV-2014-LarrazNORR #using: Proving Non-termination Using Max-SMT (DL, KN, AO, ERC, AR), pp. 779–796.
CAV-2014-Voronkov #architecture #first-order #named #theorem proving: AVATAR: The Architecture for First-Order Theorem Provers (AV), pp. 696–710.
ICLP-J-2014-PimentelON #concurrent #constraints #programming: A Proof Theoretic Study of Soft Concurrent Constraint Programming (EP, CO, VN), pp. 649–663.
IJCAR-2014-BaumgartnerBW #finite #quantifier #theorem proving: Finite Quantification in Hierarchic Theorem Proving (PB, JB, UW), pp. 152–167.
IJCAR-2014-BeesonW #geometry: OTTER Proofs in Tarskian Geometry (MB, LW), pp. 495–510.
IJCAR-2014-BeyersdorffC #complexity #theorem proving: The Complexity of Theorem Proving in Circumscription and Minimal Entailment (OB, LC), pp. 403–417.
IJCAR-2014-BoudouFP #named: Skeptik: A Proof Compression System (JB, AF, BWP), pp. 374–380.
IJCAR-2014-GieslBEFFOPSSST #automation #source code #termination: Proving Termination of Programs Automatically with AProVE (JG, MB, FE, FF, CF, CO, MP, PSK, TS, SS, RT), pp. 184–191.
IJCAR-2014-GoreTW #logic #theorem proving #using: A History-Based Theorem Prover for Intuitionistic Propositional Logic Using Global Caching: IntHistGC System Description (RG, JT, JW), pp. 262–268.
IJCAR-2014-HeuleSB #preprocessor: A Unified Proof System for QBF Preprocessing (MH, MS, AB), pp. 91–106.
IJCAR-2014-NigamRL #automation #named #permutation: Quati: An Automated Tool for Proving Permutation Lemmas (VN, GR, LL), pp. 255–261.
IJCAR-2014-Otten #first-order #logic #named: MleanCoP: A Connection Prover for First-Order Modal Logic (JO), pp. 269–276.
IJCAR-2014-StroderGBFFHS #memory management #pointer #safety #source code #termination: Proving Termination and Memory Safety for Programs with Pointer Arithmetic (TS, JG, MB, FF, CF, JH, PSK), pp. 208–223.
ISSTA-2014-Chen #constraints #program analysis #reuse #scalability: Reusing constraint proofs for scalable program analysis (MC), pp. 449–452.
LICS-CSL-2014-Ehrhard #correctness: A new correctness criterion for MLL proof nets (TE), p. 10.
LICS-CSL-2014-HeijltjesH #equivalence: No proof nets for MLL with units: proof equivalence in MLL is PSPACE-complete (WH, RH), p. 10.
LICS-CSL-2014-Mahboubi #order #theorem: Computer-checked mathematics: a formal proof of the odd order theorem (AM), p. 1.
SAT-2014-BalabanovWJ: QBF Resolution Systems and Their Proof Complexities (VB, MW, JHRJ), pp. 154–169.
SAT-2014-BelovHM #using: MUS Extraction Using Clausal Proofs (AB, MH, JMS), pp. 48–57.
SAT-2014-IstrateC #complexity #theorem: Proof Complexity and the Kneser-Lovász Theorem (GI, AC), pp. 138–153.
SAT-2014-MiksaN: Long Proofs of (Seemingly) Simple Formulas (MM, JN), pp. 121–137.
SAT-2014-Nordstrom #complexity #overview #satisfiability: A (Biased) Proof Complexity Survey for SAT Practitioners (JN), pp. 1–6.
SAT-2014-WetzlerHH #named #performance #using: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs (NW, MH, WAHJ), pp. 422–429.
TAP-2014-KosmatovLA #case study #testing #verification: A Case Study on Verification of a Cloud Hypervisor by Proof and Structural Testing (NK, ML, CA), pp. 158–164.
DLT-2013-Regnault #automaton #probability: Proof of a Phase Transition in Probabilistic Cellular Automata (DR), pp. 433–444.
ICALP-v1-2013-LauriaPRT #complexity #graph: The Complexity of Proving That a Graph Is Ramsey (ML, PP, VR, NT), pp. 684–695.
ICALP-v2-2013-BecchettiBDKM #bound #complexity #convergence: Physarum Can Compute Shortest Paths: Convergence Proofs and Complexity Bounds (LB, VB, MD, AK, KM), pp. 472–483.
ICALP-v2-2013-Stirling #λ-calculus: Proof Systems for Retracts in Simply Typed λ Calculus (CS), pp. 398–409.
LATA-2013-RotBR #equivalence #induction: Coinductive Proof Techniques for Language Equivalence (JR, MMB, JJMMR), pp. 480–492.
IFM-2013-Abrial #source code: From Z to B and then Event-B: Assigning Proofs to Meaningful Programs (JRA), pp. 1–15.
RTA-2013-FelgenhauerO #diagrams #order: Proof Orders for Decreasing Diagrams (BF, VvO), pp. 174–189.
RTA-2013-WinklerZM #automation #sequence #termination: Beyond Peano Arithmetic — Automatically Proving Termination of the Goodstein Sequence (SW, HZ, AM), pp. 335–351.
TLCA-2013-Herbelin: Proving with Side Effects (HH), p. 2.
KEOD-2013-AkamaN #problem: Embedding Proof Problems into Query-answering Problems and Problem Solving by Equivalent Transformation (KA, EN), pp. 253–260.
SEKE-2013-Alegroth #concept #random #testing #user interface #visual notation: Random Visual GUI Testing: Proof of Concept (EA), pp. 178–183.
HILT-2013-Taft #concurrent #named #parallel #safety #source code #thread #tutorial: Tutorial: proving safety of parallel / multi-threaded programs (STT), pp. 1–2.
PLDI-2013-Qiu0SM: Natural proofs for structure, data, and separation (XQ, PG, AS, PM), pp. 231–242.
POPL-2013-Gonthier #order #theorem: Engineering mathematics: the odd order theorem proof (GG), pp. 1–2.
POPL-2013-HurNDV #induction #power of: The power of parameterization in coinductive proof (CKH, GN, DD, VV), pp. 193–206.
POPL-2013-ParkSP #theorem proving: A theorem prover for Boolean BI (JP, JS, SP), pp. 219–232.
PPDP-2013-KrienerKB #coq #prolog #semantics: Proofs you can believe in: proving equivalences between Prolog semantics in Coq (JK, AK, SB), pp. 37–48.
SAC-PL-J-2010-PopeeaC13 #analysis #debugging #safety: Dual analysis for proving safety and finding bugs (CP, WNC), pp. 390–411.
ASE-2013-HuangMM #smt #using: Proving MCAPI executions are correct using SMT (YH, EM, JM), pp. 26–36.
ESEC-FSE-2013-Nori0 #termination #testing: Termination proofs from tests (AVN, RS), pp. 246–256.
ESOP-2013-FilliatreP #named #source code #why: Why3 — Where Programs Meet Provers (JCF, AP), pp. 125–128.
ESOP-2013-WickersonDP #logic: Ribbon Proofs for Separation Logic (JW, MD, MJP), pp. 189–208.
FoSSaCS-2013-MioS #composition #concurrent #probability #process #verification: A Proof System for Compositional Verification of Probabilistic Concurrent Processes (MM, AS), pp. 161–176.
STOC-2013-Ben-SassonCGT #on the #performance: On the concrete efficiency of probabilistically-checkable proofs (EBS, AC, DG, ET), pp. 585–594.
STOC-2013-RothblumVW #interactive #proximity #sublinear: Interactive proofs of proximity: delegating computation in sublinear time (GNR, SPV, AW), pp. 793–802.
STOC-2013-Williams: Natural proofs versus derandomization (RW), pp. 21–30.
TACAS-2013-ChristHN: Proof Tree Preserving Interpolation (JC, JH, AN), pp. 124–138.
TACAS-2013-CookSZ #termination: Ramsey vs. Lexicographic Termination Proving (BC, AS, FZ), pp. 47–61.
TACAS-2013-LiDDMS #abduction #composition #synthesis: Synthesis of Circular Compositional Program Proofs via Abduction (BL, ID, TD, KLM, MS), pp. 370–384.
CADE-2013-ChihaniMR #first-order #logic: Foundational Proof Certificates in First-Order Logic (ZC, DM, FR), pp. 162–177.
CADE-2013-ClaessenJRS #automation #induction #using: Automating Inductive Proofs Using Theory Exploration (KC, MJ, DR, NS), pp. 392–406.
CADE-2013-HawblitzelKLR #automation #source code #theorem proving #towards #using: Towards Modularly Comparing Programs Using Automated Theorem Provers (CH, MK, SKL, HR), pp. 282–299.
CADE-2013-KaliszykU #named #re-engineering: PRocH: Proof Reconstruction for HOL Light (CK, JU), pp. 267–274.
CADE-2013-Mayer #hybrid #logic #transitive: A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies (MCM), pp. 76–90.
CADE-2013-WilliamsK #problem #reduction #satisfiability: Propositional Temporal Proving with Reductions to a SAT Problem (RW, BK), pp. 421–435.
CAV-2013-BrockschmidtCF #termination: Better Termination Proving through Cooperation (MB, BC, CF), pp. 413–429.
CAV-2013-DragoiGH #automation #concurrent: Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates (CD, AG, TAH), pp. 174–190.
CAV-2013-GantyG #termination: Proving Termination Starting from the End (PG, SG), pp. 397–412.
CAV-2013-KovacsV #first-order #theorem proving: First-Order Theorem Proving and Vampire (LK, AV), pp. 1–35.
CAV-2013-MeierSCB #analysis #protocol #security: The TAMARIN Prover for the Symbolic Analysis of Security Protocols (SM, BS, CC, DAB), pp. 696–701.
CAV-2013-WonischSW #source code: Programs from Proofs — A PCC Alternative (DW, AS, HW), pp. 912–927.
CSL-2013-FortierS #semantics: Cuts for circular proofs: semantics and cut-elimination (JF, LS), pp. 248–262.
CSL-2013-GhasemlooC #bound: Theories for Subexponential-size Bounded-depth Frege Proofs (KG, SAC), pp. 296–315.
CSL-2013-Kikuchi #nondeterminism #normalisation #λ-calculus: Proving Strong Normalisation via Non-deterministic Translations into Klop’s Extended λ-Calculus (KK), pp. 395–414.
ISSTA-2013-Bonacchi #case study #safety: Formal safety proof: a real case study in a railway interlocking system (AB0), pp. 378–381.
LICS-2013-Halpern #first-order #logic #security #using: From Qualitative to Quantitative Proofs of Security Properties Using First-Order Conditional Logic (JYH), pp. 2–3.
LICS-2013-HoffmannMS #reasoning: Quantitative Reasoning for Proving Lock-Freedom (JH, MM, ZS), pp. 124–133.
SAT-2013-Atserias #algebra #bound #problem: The Proof-Search Problem between Bounded-Width Resolution and Bounded-Degree Semi-algebraic Proofs (AA), pp. 1–17.
SAT-2013-Beyersdorff #complexity #logic #theorem proving: The Complexity of Theorem Proving in Autoepistemic Logic (OB), pp. 365–376.
SAT-2013-Johannsen #exponential #learning: Exponential Separations in a Hierarchy of Clause Learning Proof Systems (JJ), pp. 40–51.
SAT-2013-Lauria #bound #rank #theorem: A Rank Lower Bound for Cutting Planes Proofs of Ramsey’s Theorem (ML), pp. 351–364.
TAP-2013-KosmatovPS #source code #tutorial: A Lesson on Proof of Programs with Frama-C. Invited Tutorial Paper (NK, VP, JS), pp. 168–177.
VMCAI-2013-Podelski #automaton: Automata as Proofs (AP), pp. 13–14.
SIGITE-2012-EavesS #as a service #concept: Desktop as a service proof of concept (AE, MS), pp. 85–86.
LATA-2012-Hetzl: Applying Tree Languages in Proof Theory (SH), pp. 301–312.
FM-2012-CousineauDLMRV: TLA + Proofs (DC, DD, LL, SM, DR, HV), pp. 147–154.
IFM-2012-LensinkSE #concurrent #framework #source code: A Proof Framework for Concurrent Programs (LL, SS, MCJDvE), pp. 174–190.
RTA-2012-CousineauH #semantics: A Semantic Proof that Reducibility Candidates entail Cut Elimination (DC, OH), pp. 133–148.
SEFM-2012-MatichukM #automation #specification #using: Extensible Specifications for Automatic Re-use of Specifications and Proofs (DM, TCM), pp. 333–341.
Haskell-2012-Swierstra #case study #coq #experience #programming: xmonad in Coq (experience report): programming a window manager in a proof assistant (WS), pp. 131–136.
ICFP-2012-StewartBA #theorem proving: Verified heap theorem prover by paramodulation (GS, LB, AWA), pp. 3–14.
ICFP-2012-VytiniotisJM #compilation #fault #similarity: Equality proofs and deferred type errors: a compiler pearl (DV, SLPJ, JPM), pp. 341–352.
IFL-2012-WaltS: Engineering Proof by Reflection in Agda (PvdW, WS), pp. 157–173.
CHI-2012-LazarFBMWHOE #approach #interactive: The SoundsRight CAPTCHA: an improved approach to audio human interaction proofs for blind users (JL, JF, TB, GM, BW, JH, AO, NE), pp. 2267–2276.
KR-2012-TosattoBTV #semantics: Abstract Normative Systems: Semantics and Proof Theory (SCT, GB, LWNvdT, SV).
HILT-2012-Leino12a #using #verification #why: Program proving using intermediate verification languages (IVLs) like boogie and why3 (KRML), pp. 25–26.
LOPSTR-2012-Seki #logic programming #program transformation #source code: Proving Properties of Co-logic Programs with Negation by Program Transformations (HS), pp. 213–227.
PLDI-2012-CarbinKMR #approximate #nondeterminism #source code: Proving acceptability properties of relaxed nondeterministic approximate programs (MC, DK, SM, MCR), pp. 169–180.
PLDI-2012-GrebenshchikovLPR #verification: Synthesizing software verifiers from proof rules (SG, NPL, CP, AR), pp. 405–416.
POPL-2012-HoderKV #game studies: Playing in the grey area of proofs (KH, LK, AV), pp. 259–272.
POPL-2012-MadhusudanQS #induction #recursion: Recursive proofs for inductive tree data-structures (PM, XQ, AS), pp. 123–136.
POPL-2012-Moore #theorem proving: Meta-level features in an industrial-strength theorem prover (JSM), pp. 425–426.
POPL-2012-StampoulisS: Static and user-extensible proof checking (AS, ZS), pp. 273–284.
SAS-2012-BartheGB #encryption: Computer-Aided Cryptographic Proofs (GB, BG, SZB), pp. 1–2.
SAS-2012-ChenFM #linear #termination: Termination Proofs for Linear Simple Loops (HYC, SF, SM), pp. 422–438.
SAS-2012-Midtgaard0M: A Structural Soundness Proof for Shivers’s Escape Technique — A Case for Galois Connections (JM, MDA, MM), pp. 352–369.
DAC-2012-PurandareAH #correctness #regular expression: Proving correctness of regular expression accelerators (MP, KA, CH), pp. 350–355.
STOC-2012-AzarM: Rational proofs (PDA, SM), pp. 1017–1028.
STOC-2012-BarakBHKSZ: Hypercontractivity, sum-of-squares proofs, and their applications (BB, FGSLB, AWH, JAK, DS, YZ), pp. 307–326.
STOC-2012-HrubesT: Short proofs for the determinant identities (PH, IT), pp. 193–212.
STOC-2012-HuynhN #communication #complexity #on the #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.
TACAS-2012-HolzerKSTV #contest #reachability #using: Proving Reachability Using FShell — (Competition Contribution) (AH, DK, CS, MT, HV), pp. 538–541.
TACAS-2012-PopeeaR #composition #concurrent #multi #source code #termination #thread: Compositional Termination Proofs for Multi-threaded Programs (CP, AR), pp. 237–251.
TACAS-2012-SonnexDE #automation #data type #named #recursion: Zeno: An Automated Prover for Properties of Recursive Data Structures (WS, SD, SE), pp. 407–421.
TACAS-2012-UlbrichGGT #alloy #specification: A Proof Assistant for Alloy Specifications (MU, UG, AAEG, MT), pp. 422–436.
CAV-2012-BrockschmidtMOG #automation #java #source code #termination: Automated Termination Proofs for Java Programs with Cyclic Data (MB, RM, CO, JG), pp. 105–122.
CAV-2012-EsparzaGK #probability #source code #termination #using: Proving Termination of Probabilistic Programs Using Patterns (JE, AG, SK), pp. 123–138.
CSL-2012-Cook #complexity: Connecting Complexity Classes, Weak Formal Theories, and Propositional Proof Systems (SAC), pp. 9–11.
CSL-2012-Kuroda #axiom #bound #concept: Axiomatizing proof tree concepts in Bounded Arithmetic (SK), pp. 440–454.
CSL-2012-Rabinovich #theorem: A Proof of Kamp’s theorem (AR), pp. 516–527.
IJCAR-2012-Brown #automation #higher-order #named: Satallax: An Automatic Higher-Order Prover (CEB), pp. 111–117.
IJCAR-2012-EmmesEG #automation: Proving Non-looping Non-termination Automatically (FE, TE, JG), pp. 225–240.
IJCAR-2012-JacquelBDD #automation #deduction #modulo theories #theorem proving #using #verification: Tableaux Modulo Theories Using Superdeduction — An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover (MJ, KB, DD, CD), pp. 332–338.
IJCAR-2012-UrbasJ #named: Diabelli: A Heterogeneous Proof System (MU, MJ), pp. 559–566.
LICS-2012-Herbelin #logic: A Constructive Proof of Dependent Choice, Compatible with Classical Logic (HH), pp. 365–374.
LICS-2012-Platzer12a #hybrid: The Complete Proof Theory of Hybrid Systems (AP), pp. 541–550.
LICS-2012-TraytelPB #category theory #composition #data type #higher-order #logic #theorem proving: Foundational, Compositional (Co)datatypes for Higher-Order Logic: Category Theory Applied to Theorem Proving (DT, AP, JCB), pp. 596–605.
VMCAI-2012-Nipkow #education #semantics: Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs (TN), pp. 24–38.
VLDB-2012-CormodeTY11 #interactive #streaming #verification: Verifying Computations with Streaming Interactive Proofs (GC, JT, KY), pp. 25–36.
LATA-2011-Leroux #problem #reachability #self: Vector Addition System Reachability Problem: A Short Self-contained Proof (JL), pp. 41–64.
RTA-2011-AotoT #confluence #term rewriting: A Reduction-Preserving Completion for Proving Confluence of Non-Terminating Term Rewriting Systems (TA, YT), pp. 91–106.
RTA-2011-BrockschmidtOG #bytecode #composition #java #recursion #source code #term rewriting #termination: Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting (MB, CO, JG), pp. 155–170.
RTA-2011-ContejeanCFPU #automation: Automated Certified Proofs with CiME3 (EC, PC, JF, OP, XU), pp. 21–30.
RTA-2011-MoserS #complexity #dependence #framework #multi #recursion #termination: Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity (GM, AS), pp. 235–250.
RTA-2011-NeurauterM #matrix #term rewriting #termination: Revisiting Matrix Interpretations for Proving Termination of Term Rewriting (FN, AM), pp. 251–266.
RTA-2011-Weirich #source code: Combining Proofs and Programs (SW), p. 9.
RTA-2011-ZantemaE #automation #similarity: Proving Equality of Streams Automatically (HZ, JE), pp. 393–408.
SEFM-2011-ErnstSR #analysis #empirical #interactive #theorem proving #verification: Verification of B + Trees: An Experiment Combining Shape Analysis and Interactive Theorem Proving (GE, GS, WR), pp. 188–203.
SEFM-2011-JacquelBDD #automation #theorem proving #using #verification: Verifying B Proof Rules Using Deep Embedding and Automated Theorem Proving (MJ, KB, DD, CD), pp. 253–268.
TLCA-2011-Gimenez #difference #linear #logic #normalisation: Realizability Proof for Normalization of Full Differential Linear Logic (SG), pp. 107–122.
TLCA-2011-Weirich #source code: Combining Proofs and Programs (SW), p. 9.
ICFP-2011-GonthierZND #ad hoc #automation #how: How to make ad hoc proof automation less ad hoc (GG, BZ, AN, DD), pp. 163–175.
ICFP-2011-HinzeJ #category theory #fixpoint: Proving the unique fixed-point principle correct: an adventure with category theory (RH, DWHJ), pp. 359–371.
MoDELS-2011-JacksonLB #automation #metamodelling #reasoning #specification: Reasoning about Metamodeling with Formal Specifications and Automatic Proofs (EKJ, TL, DB), pp. 653–667.
LOPSTR-2011-CaballeroRVM #debugging #declarative #maude: Simplifying Questions in Maude Declarative Debugger by Transforming Proof Trees (RC, AR, AV, NMO), pp. 73–89.
LOPSTR-2011-Seki #logic programming #source code: Proving Properties of Co-Logic Programs by Unfold/Fold Transformations (HS), pp. 205–220.
PLDI-2011-PerezR #calculus #logic #theorem proving: Separation logic + superposition calculus = heap theorem prover (JANP, AR), pp. 556–566.
POPL-2011-Leroux #problem #reachability #self: Vector addition system reachability problem: a short self-contained proof (JL), pp. 307–316.
PPDP-2011-Guenot #reduction #λ-calculus: Nested proof search as reduction in the λ-calculus (NG), pp. 183–194.
ESEC-FSE-2011-ChaudhuriGLN #robust #source code: Proving programs robust (SC, SG, RL, SN), pp. 102–112.
SAC-2011-BackP #invariant #semantics #source code: Semantics and proof rules of invariant based programs (RJB, VP), pp. 1658–1665.
SAC-2011-Blech #encryption #logic #security: Proving the security of ElGamal encryption via indistinguishability logic (JOB), pp. 1625–1632.
PDP-2011-VerbeekS #algorithm #concurrent #network #performance: A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free (FV, JS), pp. 3–10.
PPoPP-2011-BotincanDDP #automation #memory management #safety: Automatic safety proofs for asynchronous memory operations (MB, MD, AFD, MJP), pp. 313–314.
ESOP-2011-BieniusaT #memory management #transaction: Proving Isolation Properties for Software Transactional Memory (AB, PT), pp. 38–56.
STOC-2011-KawarabayashiW #algorithm #composition #graph: A simpler algorithm and shorter proof for the graph minor decomposition (KiK, PW), pp. 451–458.
TACAS-2011-ChamarthiDMV #theorem proving: The ACL2 Sedan Theorem Proving System (HRC, PCD, PM, DV), pp. 291–295.
CADE-2011-AspertiRCT #interactive #theorem proving: The Matita Interactive Theorem Prover (AA, WR, CSC, ET), pp. 64–69.
CADE-2011-BohmeM #automation #challenge #data type: Heaps and Data Structures: A Challenge for Automated Provers (SB, MM), pp. 177–191.
CADE-2011-BrotherstonDP #automation #logic: Automated Cyclic Entailment Proofs in Separation Logic (JB, DD, RLP), pp. 131–146.
CADE-2011-Brown #higher-order #problem #satisfiability #sequence #theorem proving: Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems (CEB), pp. 147–161.
CADE-2011-Cook #liveness #roadmap #termination: Advances in Proving Program Termination and Liveness (BC), p. 4.
CADE-2011-FontaineMP: Compression of Propositional Resolution Proofs via Partial Regularization (PF, SM, BWP), pp. 237–251.
CADE-2011-SchneiderS #automation #first-order #ontology #owl #reasoning #theorem proving #using: Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving (MS, GS), pp. 461–475.
CAV-2011-BalabanovJ #evaluation: Resolution Proofs and Skolem Functions in QBF Evaluation and Applications (VB, JHRJ), pp. 149–164.
LICS-2011-ChurchillLM #game studies #imperative #semantics #source code: Imperative Programs as Proofs via Game Semantics (MC, JL, GM), pp. 65–74.
LICS-2011-Heijltjes #linear #logic: Proof Nets for Additive Linear Logic with Units (WH), pp. 207–216.
LICS-2011-Pitassi #complexity #overview #state of the art: Propositional Proof Complexity: A Survey on the State of the Art, Including Some Recent Results (TP), p. 119.
TAP-2011-Gaudel #modelling #source code #testing: Checking Models, Proving Programs, and Testing Systems (MCG), pp. 1–13.
TAP-2011-Godefroid #testing: Tests from Proofs (PG), p. 14.
VMCAI-2011-CookFKP #biology: Proving Stabilization of Biological Systems (BC, JF, EK, NP), pp. 134–149.
VMCAI-2011-PiskacW #automation #termination: Decision Procedures for Automating Termination Proofs (RP, TW), pp. 371–386.
ICALP-v1-2010-AtseriasM #game studies: Mean-Payoff Games and Propositional Proofs (AA, ENM), pp. 102–113.
ICALP-v1-2010-Ito #approximate: Polynomial-Space Approximation of No-Signaling Provers (TI), pp. 140–151.
ICALP-v2-2010-ChenF #logic #on the: On p-Optimal Proof Systems and Logics for PTIME (YC, JF), pp. 321–332.
LATA-2010-LetichevskySS #automaton #equivalence #finite #multi #problem #using: The Equivalence Problem of Deterministic Multitape Finite Automata: A New Proof of Solvability Using a Multidimensional Tape (AAL, ASS, SKS), pp. 392–402.
IFM-2010-Stratulat #induction: Integrating Implicit Induction Proofs into Certified Proof Environments (SS), pp. 320–335.
RTA-2010-Aoto #automation #confluence #diagrams: Automated Confluence Proof by Decreasing Diagrams based on Rule-Labelling (TA), pp. 7–16.
RTA-2010-GuglielmiGP #calculus: A Proof Calculus Which Reduces Syntactic Bureaucracy (AG, TG, MP), pp. 135–150.
RTA-2010-ZantemaR #data type #infinity: Proving Productivity in Infinite Data Structures (HZ, MR), pp. 401–416.
FLOPS-2010-NishidaS #injection #term rewriting: Proving Injectivity of Functions via Program Inversion in Term Rewriting (NN, MS), pp. 288–303.
KEOD-2010-KatsumiG #lifecycle #ontology #theorem proving: Theorem Proving in the Ontology Lifecycle (MK, MG), pp. 37–49.
KR-2010-HorridgeP #ontology #towards: From Justifications Towards Proofs for Ontology Engineering (MH, BP).
LOPSTR-2010-HerasPR #correctness #set: Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System (JH, VP, JR), pp. 37–51.
LOPSTR-2010-SakuraiA #library #named #user interface #visualisation: MikiBeta: A General GUI Library for Visualizing Proof Trees — System Description and Demonstration (KS, KA), pp. 84–98.
LOPSTR-2010-Seki #induction #on the: On Inductive Proofs by Extended Unfold/Fold Transformation Rules (HS), pp. 117–132.
PEPM-2010-ContejeanPUCPF #approach #automation #termination: A3PAT, an approach for certified automated termination proofs (EC, AP, XU, PC, OP, JF), pp. 63–72.
POPL-2010-TateSL #compilation #generative #optimisation: Generating compiler optimizations from proofs (RT, MS, SL), pp. 389–402.
PPDP-2010-Bonacina #on the #theorem proving: On theorem proving for program checking: historical perspective and recent developments (MPB), pp. 1–12.
ICSE-2010-Elmas #abstraction #concurrent #named #reduction #verification: QED: a proof system based on reduction and abstraction for the static verification of concurrent software (TE), pp. 507–508.
SAC-2010-Pham #geometry: Similar triangles and orientation in plane elementary geometry for Coq-based proofs (TMP), pp. 1268–1269.
SAC-2010-PopeeaC #analysis #debugging #safety: Dual analysis for proving safety and finding bugs (CP, WNC), pp. 2137–2143.
SAC-2010-VermolenHL #consistency #modelling #using: Proving consistency of VDM models using HOL (SV, JH, PGL), pp. 2503–2510.
SAC-2010-VogelsJP #generative #performance #verification: A machine-checked soundness proof for an efficient verification condition generator (FV, BJ, FP), pp. 2517–2522.
ESOP-2010-DeshmukhRRV #concurrent #logic: Logical Concurrency Control from Sequential Proofs (JVD, GR, VPR, KV), pp. 226–245.
FASE-2010-DarvasM #consistency #using: Proving Consistency and Completeness of Model Classes Using Theory Interpretation (ÁD, PM), pp. 218–232.
FoSSaCS-2010-CateF #calculus #finite #μ-calculus: An Easy Completeness Proof for the Modal μ-Calculus on Finite Trees (BtC, GF), pp. 161–175.
STOC-2010-BeameHP #complexity: Hardness amplification in proof complexity (PB, TH, TP), pp. 87–96.
STOC-2010-KawarabayashiW #algorithm #graph #theorem: A shorter proof of the graph minor algorithm: the unique linkage theorem (KiK, PW), pp. 687–694.
TACAS-2010-ElmasQSST #abstraction #reduction: Simplifying Linearizability Proofs with Reduction and Abstraction (TE, SQ, AS, OS, ST), pp. 296–311.
WRLA-2010-GutierrezL #dependence #framework #termination: Proving Termination in the Context-Sensitive Dependency Pair Framework (RG, SL), pp. 18–34.
WRLA-2010-Shankar: Rewriting, Inference, and Proof (NS), pp. 1–14.
CAV-2010-ThakurLLBDEAR #generative: Directed Proof Generation for Machine Code (AVT, JL, AL, AB, ED, ME, TA, TWR), pp. 288–305.
CAV-2010-Vafeiadis #automation: Automatically Proving Linearizability (VV), pp. 450–464.
CSL-2010-Burel #deduction: Embedding Deduction Modulo into a Prover (GB), pp. 155–169.
CSL-2010-ChenF #on the #problem #slicing: On Slicewise Monotone Parameterized Problems and Optimal Proof Systems for TAUT (YC, JF), pp. 200–214.
CSL-2010-Krajicek: From Feasible Proofs to Feasible Computations (JK), pp. 22–31.
CSL-2010-Pous #algebra #linear #logic: Untyping Typed Algebraic Structures and Colouring Proof Nets of Cyclic Linear Logic (DP), pp. 484–498.
CSL-2010-SternagelT #dependence #termination: Signature Extensions Preserve Termination — An Alternative Proof via Dependency Pairs (CS, RT), pp. 514–528.
ICLP-2010-AlbertiGL10 #abduction #constraints #runtime: Runtime Addition of Integrity Constraints in an Abductive Proof Procedure (MA, MG, EL), pp. 4–13.
ICLP-2010-Guenot10 #calculus #linear #logic: Focused Proof Search for Linear Logic in the Calculus of Structures (NG), pp. 84–93.
IJCAR-2010-BaeldeMS #induction #theorem proving: Focused Inductive Theorem Proving (DB, DM, ZS), pp. 278–292.
IJCAR-2010-ChaudhuriDLM #safety #verification: Verifying Safety Properties with the TLA+ Proof System (KC, DD, LL, SM), pp. 142–148.
IJCAR-2010-DunchevLLWP: System Description: The Proof Transformation System CERES (TD, AL, TL, DW, BWP), pp. 427–433.
IJCAR-2010-KorovinS #named #similarity #theorem proving: iProver-Eq: An Instantiation-Based Theorem Prover with Equality (KK, CS), pp. 196–202.
IJCAR-2010-MayerC #hybrid #logic: Herod and Pilate: Two Tableau Provers for Basic Hybrid Logic (MCM, SC), pp. 255–262.
ISSTA-2010-GodefroidK #float #memory management #program analysis #safety: Proving memory safety of floating-point computations by combining static and dynamic program analysis (PG, JK), pp. 1–12.
LICS-2010-Moore #theorem proving #verification: Theorem Proving for Verification: The Early Days (JSM), p. 283.
SAT-2010-BeyersdorffMMTV #complexity #logic: Proof Complexity of Propositional Default Logic (OB, AM, SM, MT, HV), pp. 30–43.
SAT-2010-Cotton: Two Techniques for Minimizing Resolution Proofs (SC), pp. 306–312.
TAP-2010-BousquetL #analysis #evaluation #mutation testing #process: Proof Process Evaluation with Mutation Analysis (LdB, ML), pp. 55–60.
TAP-2010-Ernst #feedback #how #testing: How Tests and Proofs Impede One Another: The Need for Always-On Static and Dynamic Feedback (MDE), pp. 1–2.
TAP-2010-GogollaHK #automation #independence #invariant #ocl #testing #visualisation: Proving and Visualizing OCL Invariant Independence by Automatically Generated Test Cases (MG, LH, MK), pp. 38–54.
TAP-2010-GoldbergM #encoding #generative #testing: Generating High-Quality Tests for Boolean Circuits by Treating Tests as Proof Encoding (EG, PM), pp. 101–116.
TAP-2010-Rusu #specification #theorem proving: Combining Theorem Proving and Narrowing for Rewriting-Logic Specifications (VR), pp. 135–150.
ITiCSE-2009-Blaheta09a #array #visual notation: A visual proof of amortised-linear resizable arrays (DB), p. 338.
CIAA-2009-IosifR #termination: Automata-Based Termination Proofs (RI, AR), pp. 165–177.
LATA-2009-BeyersdorffKM #complexity #nondeterminism: Nondeterministic Instance Complexity and Proof Systems with Advice (OB, JK, SM), pp. 164–175.
RTA-2009-AotoYT #automation #confluence #term rewriting: Proving Confluence of Term Rewriting Systems Automatically (TA, JY, YT), pp. 93–102.
RTA-2009-FuhsGPSF #integer #term rewriting #termination: Proving Termination of Integer Term Rewriting (CF, JG, MP, PSK, SF), pp. 32–47.
RTA-2009-TiuG #analysis: A Proof Theoretic Analysis of Intruder Theories (AT, RG), pp. 103–117.
TLCA-2009-AbelCP #algorithm #composition #type system: A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance (AA, TC, MP), pp. 5–19.
TLCA-2009-LovasP #refinement: Refinement Types as Proof Irrelevance (WL, FP), pp. 157–171.
TLCA-2009-Strassburger #higher-order #linear #logic #multi: Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic (LS), pp. 309–324.
CEFP-2009-Devai #haskell: Embedding a Proof System in Haskell (GD), pp. 354–371.
ICFP-2009-ChlipalaMMSW #effectiveness #higher-order #imperative #interactive #source code: Effective interactive proofs for higher-order imperative programs (AC, JGM, GM, AS, RW), pp. 79–90.
ICFP-2009-Pierce #education #programming language #using: λ, the ultimate TA: using a proof assistant to teach programming language foundations (BCP), pp. 121–122.
LOPSTR-2009-IborraNV #dependence #termination: Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing (JI, NN, GV), pp. 52–66.
LOPSTR-2009-PilozziSB #approach #constraints: A Transformational Approach for Proving Properties of the CHR Constraint Store (PP, TS, MB), pp. 22–36.
LOPSTR-2009-Seki #induction #on the: On Inductive and Coinductive Proofs via Unfold/Fold Transformations (HS), pp. 82–96.
PLDI-2009-KunduTL #equivalence #optimisation #using: Proving optimizations correct using parameterized program equivalence (SK, ZT, SL), pp. 327–337.
PLDI-2009-ZeeKR #imperative #source code: An integrated proof language for imperative programs (KZ, VK, MCR), pp. 338–351.
POPL-2009-BartheGB #certification #encryption: Formal certification of code-based cryptographic proofs (GB, BG, SZB), pp. 90–101.
POPL-2009-GotsmanCPV #algorithm: Proving that non-blocking algorithms don’t block (AG, BC, MJP, VV), pp. 16–28.
PPDP-2009-BiernackaB #termination: Context-based proofs of termination for typed delimited-control operators (MB, DB), pp. 289–300.
SAS-2009-Bouissou #algorithm #correctness #implementation: Proving the Correctness of the Implementation of a Control-Command Algorithm (OB), pp. 102–119.
SAS-2009-Hurlin #automation #optimisation #parallel #source code: Automatic Parallelization and Optimization of Programs by Proof Rewriting (CH), pp. 52–68.
WRLA-2008-AndreiL09 #calculus: Strategy-Based Proof Calculus for Membrane Systems (OA, DL), pp. 23–43.
WRLA-2008-HolenJW09 #calculus #first-order #maude: Proof Search for the First-Order Connection Calculus in Maude (BH, EBJ, AW), pp. 173–188.
FASE-2009-KovacsV #array #invariant #source code #theorem proving #using: Finding Loop Invariants for Programs over Arrays Using a Theorem Prover (LK, AV), pp. 470–485.
FASE-2009-LeinoM #consistency: Proving Consistency of Pure Methods and Model Fields (KRML, RM), pp. 231–245.
STOC-2009-Moser: A constructive proof of the Lovász local lemma (RAM), pp. 343–350.
TACAS-2009-GuptaMR #testing: From Tests to Proofs (AG, RM, AR), pp. 262–276.
CADE-2009-BensaidCP #integer #named #theorem proving: Dei: A Theorem Prover for Terms with Integer Exponents (HB, RC, NP), pp. 146–150.
CADE-2009-BonacinaLM #on the #satisfiability #theorem proving: On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving (MPB, CL, LMdM), pp. 35–50.
CADE-2009-McLaughlinP #performance #theorem proving: Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method (SM, FP), pp. 230–244.
CADE-2009-Rinard #reasoning: Integrated Reasoning and Proof Choice Point Selection in the Jahob System — Mechanisms for Program Survival (MCR), pp. 1–16.
CADE-2009-Stickel #theorem proving: Building Theorem Provers (MES), pp. 306–321.
CADE-2009-SutcliffeBBT #automation #development #higher-order #logic #theorem proving: Progress in the Development of Automated Theorem Proving for Higher-Order Logic (GS, CB, CEB, FT), pp. 116–130.
CADE-2009-SwiderskiPGFS #analysis #dependence #induction #termination #theorem proving: Termination Analysis by Dependency Pairs and Inductive Theorem Proving (SS, MP, JG, CF, PSK), pp. 322–338.
CAV-2009-AbadiBC #modelling #protocol #security: Models and Proofs of Protocol Security: A Progress Report (MA, BB, HCL), pp. 35–49.
CAV-2009-DilligDA #integer #linear: Cuts from Proofs: A Complete and Practical Technique for Solving Linear Inequalities over Integers (ID, TD, AA), pp. 233–247.
CAV-2009-FuhrmannH #bound #induction #on the: On Extending Bounded Proofs to Inductive Proofs (OF, SH), pp. 278–290.
CAV-2009-Strichman #equivalence #source code #verification: Regression Verification: Proving the Equivalence of Similar Programs (OS), p. 63.
CSL-2009-Berger #induction: From Coinductive Proofs to Exact Real Arithmetic (UB), pp. 132–146.
CSL-2009-CiabattoniST: Expanding the Realm of Systematic Proof Theory (AC, LS, KT), pp. 163–178.
ICLP-2009-PilozziS #termination: Proving Termination by Invariance Relations (PP, DDS), pp. 499–503.
ICLP-2009-PilozziS09a #automation #termination: Automating Termination Proofs for CHR (PP, DDS), pp. 504–508.
ICST-2009-PostS #bound #equivalence #functional #implementation #model checking #using: Proving Functional Equivalence of Two AES Implementations Using Bounded Model Checking (HP, CS), pp. 31–40.
LICS-2009-LiangM #calculus: A Unified Sequent Calculus for Focused Proofs (CL, DM), pp. 355–364.
SAT-2009-Gelder: Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces (AVG), pp. 141–146.
TestCom-FATES-2009-SubramaniamXGP #approach #testing #theorem proving #using: An Approach for Test Selection for EFSMs Using a Theorem Prover (MS, LX, BG, ZP), pp. 146–162.
VMCAI-2009-AmjadB #analysis #automation #towards: Towards Automatic Stability Analysis for Rely-Guarantee Proofs (HA, RB), pp. 14–28.
EDM-2008-BarnesSLC #case study #logic #student #using: A pilot study on logic proof tutoring using hints generated from historical student data (TB, JCS, LL, MJC), pp. 197–201.
DLT-2008-HromkovicS #automaton #bound #nondeterminism #on the: On the Hardness of Determining Small NFA’s and of Proving Lower Bounds on Their Sizes (JH, GS), pp. 34–55.
ICALP-A-2008-Yin #complexity #nondeterminism: Cell-Probe Proofs and Nondeterministic Cell-Probe Complexity (YY), pp. 72–83.
LATA-2008-KorpM #bound #dependence #term rewriting #termination: Match-Bounds with Dependency Pairs for Proving Termination of Rewrite Systems (MK, AM), pp. 321–332.
FM-2008-McIverMG #probability #refinement: Proofs and Refutations for Probabilistic Refinement (AKM, CCM, CG), pp. 100–115.
RTA-2008-MoserS #polynomial #using: Proving Quadratic Derivational Complexities Using Context Dependent Interpretations (GM, AS), pp. 276–290.
RTA-2008-Toyama #lisp #recursion #term rewriting #termination: Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations (YT), pp. 381–391.
RTA-2008-UrbanZ: Revisiting Cut-Elimination: One Difficult Proof Is Really a Proof (CU, BZ), pp. 409–424.
SEFM-2008-BartheKPS #hybrid #verification: Preservation of Proof Pbligations for Hybrid Verification Methods (GB, CK, DP, JSF), pp. 127–136.
SEFM-2008-GuoS #finite #impact analysis #state machine #theorem proving #using: Formal Change Impact Analyses of Extended Finite State Machines Using a Theorem Prover (BG, MS), pp. 335–344.
FLOPS-2008-AbelCD #algebra #on the #type system: On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory (AA, TC, PD), pp. 3–13.
FLOPS-2008-PrinceGM #using: Proving Properties about Lists Using Containers (RP, NG, CM), pp. 97–112.
IFL-2008-Hinze #theorem: Scans and Convolutions — A Calculational Proof of Moessner’s Theorem (RH), pp. 1–24.
GT-VC-2007-Bruggink08 #graph transformation #termination #towards: Towards a Systematic Method for Proving Termination of Graph Transformation Systems (HJSB), pp. 23–38.
ICGT-2008-Pennemann #theorem proving: Resolution-Like Theorem Proving for High-Level Conditions (KHP), pp. 289–304.
KR-2008-Lin: Proving Goal Achievability (FL), pp. 621–628.
KR-2008-RenzL #automation #calculus #complexity: Automated Complexity Proofs for Qualitative Spatial and Temporal Calculi (JR, JJL), pp. 715–723.
ECMDA-FA-2008-MohagheghiD #case study #experience #industrial #overview: Where Is the Proof? — A Review of Experiences from Applying MDE in Industry (PM, VD), pp. 432–443.
PEPM-2008-SaabasU #optimisation: Proof optimization for partial redundancy elimination (AS, TU), pp. 91–101.
PEPM-2008-Voigtlander #correctness #theorem: Proving correctness via free theorems: the case of the destroy/build-rule (JV), pp. 13–20.
POPL-2008-BrotherstonBC #logic #termination: Cyclic proofs of program termination in separation logic (JB, RB, CC), pp. 101–112.
POPL-2008-GuptaHMRX: Proving non-termination (AG, TAH, RM, AR, RGX), pp. 147–158.
PPDP-2008-MontenegroPS #correctness #memory management #type system: A type system for safe memory management and its proof of correctness (MM, RP, CS), pp. 152–162.
PPDP-2008-PientkaD #programming: Programming with proofs and explicit contexts (BP, JD), pp. 163–173.
PPDP-2008-SilvaO #functional #prototype #quote: “Galculator”: functional prototype of a Galois-connection based proof assistant (PFS, JNO), pp. 44–55.
SAS-2008-ConwayDNB #analysis #fault #pointer: Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors (CLC, DD, KSN, CB), pp. 62–77.
ASE-2008-HartKGCL #abstraction #refinement: Augmenting Counterexample-Guided Abstraction Refinement with Proof Templates (TEH, KK, AG, MC, DL), pp. 387–390.
ASE-2008-HartKGCL08a #model checking #named: PtYasm: Software Model Checking with Proof Templates (TEH, KK, AG, MC, DL), pp. 479–480.
SAC-2008-AbedMS #analysis #graph #multi #reachability #theorem proving #using: Reachability analysis using multiway decision graphs in the HOL theorem prover (SA, OAM, GAS), pp. 333–338.
SAC-2008-Michelucci #geometry #theorem #word: Isometry group, words and proofs of geometric theorems (DM), pp. 1821–1825.
FASE-2008-BruckerW #higher-order #named #ocl #uml: HOL-OCL: A Formal Proof Environment for UML/OCL (ADB, BW), pp. 97–100.
STOC-2008-GoldwasserKR #interactive: Delegating computation: interactive proofs for muggles (SG, YTK, GNR), pp. 113–122.
STOC-2008-ShaltielV: Hardness amplification proofs require majority (RS, EV), pp. 589–598.
TACAS-2008-ClarkeTV #abstraction #concurrent #framework #model checking: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems (EMC, MT, HV), pp. 33–47.
TACAS-2008-McMillan #generative #invariant #quantifier #using: Quantified Invariant Generation Using an Interpolating Saturation Prover (KLM), pp. 413–427.
TACAS-2008-Moskal #smt: Rocket-Fast Proof Checking for SMT Solvers (MM), pp. 486–500.
SMT-2007-BongioKLLM08 #encoding #first-order #smt: Encoding First Order Proofs in SMT (JB, CK, HL, CL, REM), pp. 71–84.
CAV-2008-CohenN #concurrent #linear #source code: Local Proofs for Linear-Time Properties of Concurrent Programs (AC, KSN), pp. 149–161.
CAV-2008-CookGLRS #termination: Proving Conditional Termination (BC, SG, TLA, AR, MS), pp. 328–340.
CAV-2008-Harrison #theorem proving #verification: Theorem Proving for Verification (JH), pp. 11–18.
CAV-2008-MeikleF #approach #verification: Prover’s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-B (LIM, JDF), pp. 309–313.
CAV-2008-WienandWSKG #algebra #approach #correctness: An Algebraic Approach for Proving Data Correctness in Arithmetic Data Paths (OW, MW, DS, WK, GMG), pp. 473–486.
CSL-2008-Nguyen #using: Proving Infinitude of Prime Numbers Using Binomial Coefficients (PN), pp. 184–198.
CSL-2008-Thomas #decidability #model transformation #monad: Model Transformations in Decidability Proofs for Monadic Theories (WT), pp. 23–31.
ICLP-2008-NearBF #declarative #first-order #logic #named #theorem proving: αleanTAP: A Declarative Theorem Prover for First-Order Classical Logic (JPN, WEB, DPF), pp. 238–252.
ICLP-2008-Saurin #interactive #programming #towards: Towards Ludics Programming: Interactive Proof Search (AS), pp. 253–268.
IJCAR-2008-BartheGP #java #virtual machine: Preservation of Proof Obligations from Java to the Java Virtual Machine (GB, BG, MP), pp. 83–99.
IJCAR-2008-BenzmullerPTF #automation #higher-order #logic #named #theorem proving: LEO-II — A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (CB, LCP, FT, AF), pp. 162–170.
IJCAR-2008-Gacek #interactive #theorem proving: The Abella Interactive Theorem Prover (AG), pp. 154–161.
IJCAR-2008-Korovin #first-order #logic #named #theorem proving: iProver — An Instantiation-Based Theorem Prover for First-Order Logic (KK), pp. 292–298.
IJCAR-2008-KremerMT #protocol: Proving Group Protocols Secure Against Eavesdroppers (SK, AM, RT), pp. 116–131.
IJCAR-2008-Melquiond #bound: Proving Bounds on Real-Valued Functions with Computations (GM), pp. 2–17.
IJCAR-2008-Otten #agile #logic #performance #theorem proving: leanCoP 2.0and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (JO), pp. 283–291.
IJCAR-2008-PerezV #effectiveness #logic: Proof Systems for Effectively Propositional Logic (JANP, AV), pp. 426–440.
IJCAR-2008-PlatzerQ #hybrid #named #theorem proving: KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (AP, JDQ), pp. 171–178.
ISSTA-2008-BeckmanNRS #testing: Proofs from tests (NEB, AVN, SKR, RJS), pp. 3–14.
LICS-2008-DelandeM #approach: A Neutral Approach to Proof and Refutation in MALL (OD, DM), pp. 498–508.
LICS-2008-LaurentM: Cut Elimination for Monomial MALL Proof Nets (OL, RM), pp. 486–497.
LICS-2008-NauroisM #correctness #multi: Correctness of Multiplicative Additive Proof Structures is NL-Complete (PJdN, VM), pp. 476–485.
LICS-2008-Riis #calculus #complexity #on the #polynomial: On the Asymptotic Nullstellensatz and Polynomial Calculus Proof Complexity (SR), pp. 272–283.
MBT-2008-BruckerBW #empirical #verification: Verifying Test-Hypotheses: An Experiment in Test and Proof (ADB, LB, BW), pp. 15–27.
TAP-2008-ClaessenS #induction: Finding Counter Examples in Induction Proofs (KC, HS), pp. 48–65.
ITiCSE-2007-StallmannBRBGH #automaton #correctness #named: ProofChecker: an accessible environment for automata theory correctness proofs (MFS, SB, RDR, SB, MCG, SDH), pp. 48–52.
ICALP-2007-DershowitzT #complexity: Complexity of Propositional Proofs Under a Promise (ND, IT), pp. 291–302.
IFM-2007-DerrickSW #refinement: Proving Linearizability Via Non-atomic Refinement (JD, GS, HW), pp. 195–214.
RTA-2007-DowekH: A Simple Proof That Super-Consistency Implies Cut Elimination (GD, OH), pp. 93–106.
RTA-2007-Kikuchi #calculus #normalisation: Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi (KK), pp. 257–272.
RTA-2007-KorpM #bound #term rewriting #termination #using: Proving Termination of Rewrite Systems Using Bounds (MK, AM), pp. 273–287.
SEFM-2007-BabicHRC #termination: Proving Termination by Divergence (DB, AJH, ZR, BC), pp. 93–102.
SEFM-2007-Cook #automation #concurrent #source code: Automatically Proving Concurrent Programs Correct (BC), pp. 269–272.
SEFM-2007-FraserB #configuration management #tool support: Configurable Proof Obligations in the Frog Toolkit (SF, RB), pp. 361–370.
SEFM-2007-Mehta #development: Supporting Proof in a Reactive Development Environment (FM), pp. 103–112.
TLCA-2007-DavidN #calculus #equation #normalisation #recursion: An Arithmetical Proof of the Strong Normalization for the λ -Calculus with Recursive Equations on Types (RD, KN), pp. 84–101.
TLCA-2007-Nakazawa #morphism #reduction: An Isomorphism Between Cut-Elimination Procedure and Proof Reduction (KN), pp. 336–350.
CEFP-2007-MolEP #functional #lazy evaluation #source code: Proving Properties of Lazy Functional Programs with Sparkle (MdM, MCJDvE, RP), pp. 41–86.
IFL-2007-HerhutSBGT #contract #dependent type #partial evaluation #towards: From Contracts Towards Dependent Types: Proofs by Partial Evaluation (SH, SBS, RB, CG, KT), pp. 254–273.
AGTIVE-2007-MolEP #reduction: A Single-Step Term-Graph Reduction System for Proof Assistants (MdM, MCJDvE, RP), pp. 184–200.
LOPSTR-2007-Codish #termination: Proving Termination with (Boolean) Satisfaction (MC), pp. 1–7.
PLDI-2007-CookPR #concurrent #termination #thread: Proving thread termination (BC, AP, AR), pp. 320–330.
POPL-2007-CookGPRV #source code: Proving that programs eventually do something good (BC, AG, AP, AR, MYV), pp. 265–276.
PPDP-2007-Lucas #termination #using: Practical use of polynomials over the reals in proofs of termination (SL), pp. 39–50.
SIGAda-2007-Maurer #ada #using: Using mathematics to improve ada compiled code, part 2: the proof (WDM), pp. 11–26.
SAC-2007-Dufourd #framework #theorem: A hypermap framework for computer-aided proofs in surface subdivisions: genus theorem and Euler’s formula (JFD), pp. 757–761.
SAC-2007-Li #abstraction #parametricity #protocol #verification: Mechanized proofs for the parameter abstraction and guard strengthening principle in parameterized verification of cache coherence protocols (YL), pp. 1534–1535.
DAC-2007-ChatterjeeMBK #equivalence #on the: On Resolution Proofs for Combinational Equivalence (SC, AM, RKB, AK), pp. 600–605.
DATE-2007-KroeningS #image #interactive #refinement #using #word: Interactive presentation: Image computation and predicate refinement for RTL verilog using word level proofs (DK, NS), pp. 1325–1330.
ESOP-2007-BessonJT #abstract interpretation: Small Witnesses for Abstract Interpretation-Based Proofs (FB, TPJ, TT), pp. 268–283.
ESOP-2007-FrancalanzaH #bisimulation #fault tolerance: A Fault Tolerance Bisimulation Proof for Consensus (AF, MH), pp. 395–410.
STOC-2007-Dantchev #complexity #rank: Rank complexity gap for Lovász-Schrijver and Sherali-Adams proof systems (SSD), pp. 311–317.
STOC-2007-Lynch #algorithm #distributed #modelling: Distributed computing theory: algorithms, impossibility results, models, and proofs (NAL), p. 247.
CADE-2007-DeshaneHJLLM #encoding #first-order #satisfiability: Encoding First Order Proofs in SAT (TD, WH, PJ, HL, CL, REM), pp. 476–491.
CADE-2007-GieslTSS #bound #termination: Proving Termination by Bounded Increase (JG, RT, SS, PSK), pp. 443–459.
CADE-2007-Harrison #automation #using: Automating Elementary Number-Theoretic Proofs Using Gröbner Bases (JH), pp. 51–66.
CADE-2007-TiwariG #logic #program analysis #theorem proving #using: Logical Interpretation: Static Program Analysis Using Theorem Proving (AT, SG), pp. 147–166.
CADE-2007-VerchinineLP #automation #deduction #verification: System for Automated Deduction (SAD): A Tool for Proof Verification (KV, AVL, AP), pp. 398–403.
CAV-2007-CohenN #safety: Local Proofs for Global Safety Properties (AC, KSN), pp. 55–67.
CAV-2007-Cook #automation #termination: Automatically Proving Program Termination (BC), p. 1.
CAV-2007-JhalaM #abstraction #array: Array Abstractions from Proofs (RJ, KLM), pp. 193–206.
CSL-2007-Abramsky #geometry #interactive: Full Completeness: Interactive and Geometric Characterizations of the Space of Proofs (SA), pp. 1–2.
CSL-2007-Beckmann #complexity #source code: Proofs, Programs and Abstract Complexity (AB), pp. 4–5.
CSL-2007-MillerN: Incorporating Tables into Proofs (DM, VN), pp. 466–480.
CSL-2007-MillerS #composition #linear #logic: From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic (DM, AS), pp. 405–419.
CSL-2007-NauroisM #correctness #exponential #multi: Correctness of Multiplicative (and Exponential) Proof Structures is NL -Complete (PJdN, VM), pp. 435–450.
ICLP-2007-PettorossiPS #automation #correctness #logic programming #program transformation: Automatic Correctness Proofs for Logic Program Transformations (AP, MP, VS), pp. 364–379.
LICS-2007-Nguyen: Separating DAG-Like and Tree-Like Proof Systems (PN), pp. 235–244.
LICS-2007-NguyenC #complexity #theorem: The Complexity of Proving the Discrete Jordan Curve Theorem (PN, SAC), pp. 245–256.
LICS-2007-RabinST #correctness #performance: Highly Efficient Secrecy-Preserving Proofs of Correctness of Computations and Applications (MOR, RAS, CT), pp. 63–76.
MBT-2007-LedruBDA #case study: A Case Study in Matching Test and Proof Coverage (YL, LdB, FD, FA), pp. 73–84.
SAT-2007-JussilaBSKW #towards: A First Step Towards a Unified Proof Checker for QBF (TJ, AB, CS, DK, CMW), pp. 201–214.
TAP-2007-EngelH #generative #testing: Generating Unit Tests from Formal Proofs (CE, RH), pp. 169–188.
TAP-2007-Haiyan #algorithm #distributed #testing #type system: Testing and Proving Distributed Algorithms in Constructive Type Theory (QH), pp. 79–94.
TAP-2007-RummerS #calculus #java #logic #source code #using: Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic (PR, MAS), pp. 41–60.
VMCAI-2007-BouillaguetKWZR #data type #first-order #theorem proving #using #verification: Using First-Order Theorem Provers in the Jahob Data Structure Verification System (CB, VK, TW, KZ, MCR), pp. 74–88.
CIAA-2006-OnderB: XSLT Version 2.0 Is Turing-Complete: A Purely Transformation Based Proof (RO, ZB), pp. 275–276.
ICALP-v1-2006-KojevnikovI #bound #calculus: Lower Bounds of Static Lovász-Schrijver Calculus Proofs for Tseitin Tautologies (AK, DI), pp. 323–334.
ICALP-v2-2006-CorinH #encryption #game studies #hoare #logic #probability: A Probabilistic Hoare-style Logic for Game-Based Cryptographic Proofs (RC, JdH), pp. 252–263.
FM-2006-SchellhornGHR #challenge: The Mondex Challenge: Machine Checked Proofs for an Electronic Purse (GS, HG, DH, WR), pp. 16–31.
FM-2006-UmenoL #automaton #case study #protocol #safety #theorem proving #using: Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study (SU, NAL), pp. 64–80.
RTA-2006-BournezG #termination: Proving Positive Almost Sure Termination Under Strategies (OB, FG), pp. 357–371.
RTA-2006-Bruggink #finite #higher-order #product line #using: A Proof of Finite Family Developments for Higher-Order Rewriting Using a Prefix Property (HJSB), pp. 372–386.
RTA-2006-SantoFP: Structural Proof Theory as Rewriting (JES, MJF, LP), pp. 197–211.
SFM-2006-Harrison #float #theorem proving #using #verification: Floating-Point Verification Using Theorem Proving (JH), pp. 211–242.
SFM-2006-Manolios #refinement #theorem proving: Refinement and Theorem Proving (PM), pp. 176–210.
FLOPS-2006-BartheFPR #coq #reasoning #recursion: Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant (GB, JF, DP, VR), pp. 114–129.
ICFP-2006-Chlipala #composition #development #verification: Modular development of certified program verifiers with a proof assistant (AC), pp. 160–171.
ICFP-2006-Shapiro #concurrent #source code: Practical proofs of concurrent programs (MS), p. 123.
IFL-2006-Brady: Ivor, a Proof Engine (EB), pp. 145–162.
IFL-2006-Kozsik #type system: Proving Program Properties Specified with Subtype Marks (TK), pp. 163–180.
LOPSTR-2006-MantelSK #data flow #security #verification: Combining Different Proof Techniques for Verifying Information Flow Security (HM, HS, TK), pp. 94–110.
LOPSTR-2006-NguyenS #automation #named #polynomial #termination: Polytool: Proving Termination Automatically Based on Polynomial Interpretations (MTN, DDS), pp. 210–218.
PLDI-2006-CookPR #termination: Termination proofs for systems code (BC, AP, AR), pp. 415–426.
POPL-2006-Dam #decidability: Decidability and proof systems for language-based noninterference relations (MD), pp. 67–78.
POPL-2006-Leroy #certification #compilation #programming: Formal certification of a compiler back-end or: programming a compiler with a proof assistant (XL), pp. 42–54.
PPDP-2006-Sulzmann #source code: Extracting programs from type class proofs (MS), pp. 97–108.
SAS-2006-Bertrane #communication: Proving the Properties of Communicating Imperfectly-Clocked Synchronous Systems (JB), pp. 370–386.
RE-2006-Miller #development #modelling #requirements: Proving the Shalls: Requirements, Proofs, and Model-Based Development (SPM), p. 261.
ASE-2006-Futatsugi #specification #verification: Verifying Specifications with Proof Scores in CafeOBJ (KF), pp. 3–10.
ASE-2006-Jurjens #analysis #automation #java #security #source code #theorem proving #using: Security Analysis of Crypto-based Java Programs using Automated Theorem Provers (JJ), pp. 167–176.
ICSE-2006-ManoliosV #static analysis #termination #theorem proving: Integrating static analysis and general-purpose theorem proving for termination analysis (PM, DV), pp. 873–876.
DAC-2006-RawatCKSGZS #named #question: DFM: where’s the proof of value? (SR, RC, AK, JS, MG, NZ, AS), pp. 1061–1062.
DATE-DF-2006-LennardBFIUSWFRB #design #integration #specification: Industrially proving the SPIRIT consortium specifications for design chain integration (CKL, VB, SF, MI, CU, MS, JW, OF, FR, PB), pp. 142–147.
HPDC-2006-BellenotBGIKPRBLRCF #named #parallel: PROOF — The Parallel ROOT Facility (BB, RB, GG, JI, GK, AJP, FR, MB, CL, CR, PC, DF), pp. 379–380.
PPoPP-2006-VafeiadisHHS #correctness: Proving correctness of highly-concurrent linearisable objects (VV, MH, CARH, MS), pp. 129–136.
STOC-2006-Gurvits #algorithm #approach #bound: Hyperbolic polynomials approach to Van der Waerden/Schrijver-Valiant like conjectures: sharper bounds, simpler proofs and algorithmic applications (LG), pp. 417–426.
STOC-2006-NguyenV #performance: Zero knowledge with efficient provers (MHN, SPV), pp. 287–295.
STOC-2006-Nordstrom: Narrow proofs may be spacious: separating space and width in resolution (JN), pp. 507–516.
TACAS-2006-FontaineMMNT #automation #interactive #smt #towards: Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants (PF, JYM, SM, LPN, AFT), pp. 167–181.
TACAS-2006-LeueW #approach #graph #termination: A Region Graph Based Approach to Termination Proofs (SL, WW), pp. 318–333.
CAV-2006-BerdineCDO #automation #source code #termination: Automatic Termination Proofs for Programs with Shape-Shifting Heaps (JB, BC, DD, PWO), pp. 386–400.
CAV-2006-Roe #heuristic #modulo theories #smt #theorem proving: The Heuristic Theorem Prover: Yet Another SMT Modulo Theorem Prover (KR), pp. 467–470.
CSL-2006-ArtemovK #complexity #logic: Logical Omniscience Via Proof Complexity (SNA, RK), pp. 135–149.
CSL-2006-GiamberardinoF #parallel: Jump from Parallel to Sequential Proofs: Multiplicatives (PDG, CF), pp. 319–333.
ICLP-2006-PettorossiPS #constraints #logic programming #source code: Proving Properties of Constraint Logic Programs by Eliminating Existential Variables (AP, MP, VS), pp. 179–195.
IJCAR-2006-Boldo #algorithm #float: Pitfalls of a Full Floating-Point Proof: Example on the Formal Proof of the Veltkamp/Dekker Algorithms (SB), pp. 52–66.
IJCAR-2006-ConstableM #semantics #source code: Extracting Programs from Constructive HOL Proofs Via IZF Set-Theoretic Semantics (RLC, WM), pp. 162–176.
IJCAR-2006-EndrullisWZ #matrix #term rewriting #termination: Matrix Interpretations for Proving Termination of Term Rewriting (JE, JW, HZ), pp. 574–588.
IJCAR-2006-GieslST #automation #dependence #framework #termination: Automatic Termination Proofs in the Dependency Pair Framework (JG, PSK, RT), pp. 281–286.
IJCAR-2006-KozenKR #automation #category theory: Automating Proofs in Category Theory (DK, CK, ER), pp. 392–407.
IJCAR-2006-Mahboubi #algorithm #implementation #performance: Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials (AM), pp. 438–452.
IJCAR-2006-NivelleM #finite #geometry: Geometric Resolution: A Proof Procedure Based on Finite Model Search (HdN, JM), pp. 303–317.
ISSTA-2006-YorshBS #abstraction #exclamation #testing #theorem proving: Testing, abstraction, theorem proving: better together! (GY, TB, MS), pp. 145–156.
LICS-2006-CoquandS #normalisation #using: A Proof of Strong Normalisation using Domain Theory (TC, AS), pp. 307–316.
LICS-2006-Kozen #induction #probability #process: Coinductive Proof Principles for Stochastic Processes (DK), pp. 359–366.
LICS-2006-Leivant #logic #reasoning #source code: Matching Explicit and Modal Reasoning about Programs: A Proof Theoretic Delineation of Dynamic Logic (DL), pp. 157–168.
LICS-2006-MacielP #bound #composition: Conditional Lower Bound for a System of Constant-Depth Proofs with Modular Connectives (AM, TP), pp. 189–200.
SAT-2006-Gelder #metric: Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs (AVG), pp. 48–53.
SAT-2006-JussilaSB #quantifier #satisfiability: Extended Resolution Proofs for Symbolic SAT Solving with Quantification (TJ, CS, AB), pp. 54–60.
SAT-2006-KojevnikovK #algebra #complexity #strict: Complexity of Semialgebraic Proofs with Restricted Degree of Falsity (AK, ASK), pp. 11–21.
ICDAR-2005-RusuG #algorithm #interactive #recognition #using: A Human Interactive Proof Algorithm Using Handwriting Recognition (AIR, VG), pp. 967–971.
RTA-2005-BournezG #termination: Proving Positive Almost-Sure Termination (OB, FG), pp. 323–337.
RTA-2005-StumpT #algebra #similarity: The Algebra of Equality Proofs (AS, LYT), pp. 469–483.
SEFM-2005-OlssonW #correctness #imperative #induction #source code: Customised Induction Rules for Proving Correctness of Imperative Programs (OO, AW), pp. 180–189.
SEFM-2005-Trentelman #correctness #using: Proving Correctness of JavaCard DL Taclets using Bali (KT), pp. 160–169.
TLCA-2005-DavidN #normalisation #symmetry #λ-calculus #μ-calculus: Arithmetical Proofs of Strong Normalization Results for the Symmetric λμ-Calculus (RD, KN), pp. 162–178.
TLCA-2005-Hayashi #game studies #question: Can Proofs Be Animated By Games? (SH), pp. 11–22.
TLCA-2005-LamarcheS #logic: Naming Proofs in Classical Propositional Logic (FL, LS), pp. 246–261.
TLCA-2005-PrevostoB: Proof Contexts with Late Binding (VP, SB), pp. 324–338.
ICFP-2005-ChenX #programming #theorem proving: Combining programming with theorem proving (CC, HX), pp. 66–77.
IFL-2005-EekelenM #strict #tool support: Proof Tool Support for Explicit Strictness (MCJDvE, MdM), pp. 37–54.
CHI-2005-ChellapillaLSC #design #interactive: Designing human friendly human interaction proofs (HIPs) (KC, KL, PYS, MC), pp. 711–720.
SEKE-2005-OgataF #approach #liveness #verification: Proof Score Approach to Verification of Liveness Properties (KO, KF), pp. 608–613.
AdaEurope-2005-SwardB #equivalence #functional #slicing: Proving Functional Equivalence for Program Slicing in SPARK™ (RES, LCBI), pp. 105–114.
POPL-2005-LernerMRC #analysis #automation #data flow: Automated soundness proofs for dataflow analyses and transformations via local rules (SL, TDM, ER, CC), pp. 364–377.
ASE-2005-GheyiMB #approach #refactoring: A rigorous approach for proving model refactorings (RG, TM, PB), pp. 372–375.
ASE-2005-WardKA #framework #named #theorem proving: Prufrock: a framework for constructing polytypic theorem provers (JW, GK, PA), pp. 423–426.
COCV-J-2005-BlechGLM #code generation #comparison #correctness #higher-order #optimisation: Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL (JOB, SG, JL, SM), pp. 33–51.
COCV-J-2005-SalcianuA #analysis #correctness #data flow: Machine-Checkable Correctness Proofs for Intra-procedural Dataflow Analyses (AS, KA), pp. 53–68.
DAC-2005-MonyBPK: Exploiting suspected redundancy without proving it (HM, JB, VP, RK), pp. 463–466.
WRLA-2004-PalominoP05 #maude #model checking: Proving VLRL Action Properties with the Maude Model Checker (MP, IP), pp. 113–133.
ESOP-2005-CortierW #automation #protocol #security: Computationally Sound, Automated Proofs for Security Protocols (VC, BW), pp. 157–171.
FASE-2005-FuriaRMM #automation #composition #realtime: Automated Compositional Proofs for Real-Time Systems (CAF, MR, DM, AM), pp. 326–340.
FoSSaCS-2005-Cheney #logic: A Simpler Proof Theory for Nominal Logic (JC), pp. 379–394.
TACAS-2005-IsobeR #csp #refinement #theorem proving: A Generic Theorem Prover of CSP Refinement (YI, MR), pp. 108–123.
TACAS-2005-LeinoMO #quantifier #theorem proving: A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover (KRML, MM, XO), pp. 334–348.
CADE-2005-CastelliniS #first-order #logic #theorem proving: Proof Planning for First-Order Temporal Logic (CC, AS), pp. 235–249.
CADE-2005-ChaudhuriP #first-order #linear #logic #theorem proving: A Focusing Inverse Method Theorem Prover for First-Order Linear Logic (KC, FP), pp. 69–83.
CADE-2005-ContejeanC #first-order #logic #similarity: Reflecting Proofs in First-Order Logic with Equality (EC, PC), pp. 7–22.
CADE-2005-MeierM #multi #theorem proving: System Description: Multi A Multi-strategy Proof Planner (AM, EM), pp. 250–254.
CADE-2005-OgawaHO #incremental: Proving Properties of Incremental Merkle Trees (MO, EH, SO), pp. 424–440.
CAV-2005-CookKS #named #theorem proving #verification: Cogent: Accurate Theorem Proving for Program Verification (BC, DK, NS), pp. 296–300.
CSL-2005-Perron: A Propositional Proof System for Log Space (SP), pp. 509–524.
CSL-2005-Soltys #algorithm #matrix: Feasible Proofs of Matrix Properties with Csanky’s Algorithm (MS), pp. 493–508.
ICLP-2005-SarkarPC: Small Proof Witnesses for LF (SS, BP, KC), pp. 387–401.
LICS-2005-Hardin #algebra: Proof Theory for Kleene Algebra (CH), pp. 290–299.
SAT-2005-Gelder #bound #distance: Input Distance and Lower Bounds for Propositional Resolution Proof Length (AVG), pp. 282–293.
SAT-2005-HirschN #simulation #strict: Simulating Cutting Plane Proofs with Restricted Degree of Falsity by Resolution (EAH, SIN), pp. 135–142.
VMCAI-2005-Cousot #abstraction #parametricity #programming #termination: Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming (PC), pp. 1–24.
CIAA-2004-NishimuraY #automaton #finite #interactive #quantum: An Application of Quantum Finite Automata to Interactive Proof Systems (HN, TY), pp. 225–236.
ICALP-2004-Meer #theorem: Transparent Long Proofs: A First PCP Theorem for NPR (KM), pp. 959–970.
ICALP-2004-OstrovskyRS #commit #consistency #database #performance #query: Efficient Consistency Proofs for Generalized Queries on a Committed Database (RO, CR, AS), pp. 1041–1053.
ICALP-2004-Razborov: Feasible Proofs and Computations: Partnership and Fusion (AAR), pp. 8–14.
IFM-2004-EllisI #automation #integration #program analysis #theorem proving: An Integration of Program Analysis and Automated Theorem Proving (BJE, AI), pp. 67–86.
IFM-2004-Melham #functional #model checking #theorem proving: Integrating Model Checking and Theorem Proving in a Reflective Functional Language (TFM), pp. 36–39.
RTA-2004-GieslTSF #automation #termination: Automated Termination Proofs with AProVE (JG, RT, PSK, SF), pp. 210–220.
RTA-2004-LimetS #logic programming #source code #term rewriting: Proving Properties of Term Rewrite Systems via Logic Programs (SL, GS), pp. 170–184.
RTA-2004-Lucas #named #termination: mu-term: A Tool for Proving Termination of Context-Sensitive Rewriting (SL), pp. 200–209.
SEFM-2004-BeckertK #deduction #reuse #verification: Proof Reuse for Deductive Program Verification (BB, VK), pp. 77–86.
FLOPS-2004-Kikuchi #calculus #normalisation: A Direct Proof of Strong Normalization for an Extended Herbelin?s Calculus (KK), pp. 244–259.
LOPSTR-2004-WellsY #graph #synthesis: Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis (JBW, BY), pp. 262–277.
PDCL-2004-LindenstraussSS #approach #logic programming #source code #termination: Proving Termination for Logic Programs by the Query-Mapping Pairs Approach (NL, YS, AS), pp. 453–498.
PEPM-2004-DuranLMMU #equation #source code #termination: Proving termination of membership equational programs (FD, SL, JM, CM, XU), pp. 147–158.
PEPM-2004-PopeeaC #correctness #protocol #type system #verification: A type system for resource protocol verification and its correctness proof (CP, WNC), pp. 135–146.
PLDI-2004-Appel #process #revisited #social #source code #theorem: Social processes and proofs of theorems and programs, revisited (AWA), p. 170.
POPL-2004-Benton #analysis #correctness #program transformation #relational: Simple relational correctness proofs for static analyses and program transformations (NB), pp. 14–25.
POPL-2004-HenzingerJMM #abstraction: Abstractions from proofs (TAH, RJ, RM, KLM), pp. 232–244.
RE-2004-KatzR #aspect-oriented #requirements: From Aspectual Requirements to Proof Obligations for Aspect-Oriented Systems (SK, AR), pp. 48–57.
ICSE-2004-HaRCRD #case study #composition #experience #induction #realtime: Feature-Based Decomposition of Inductive Proofs Applied to Real-Time Avionics Software: An Experience Report (VH, MR, DDC, HR, BD), pp. 304–313.
ESOP-2004-FilliatreL #source code: Functors for Proofs and Programs (JCF, PL), pp. 370–384.
ESOP-2004-JiaW #distributed #source code: Modal Proofs as Distributed Programs (LJ, DW), pp. 219–233.
FoSSaCS-2004-Lucas #termination: Polynomials for Proving Termination of Context-Sensitive Rewriting (SL), pp. 318–332.
TACAS-2004-McMillan #theorem proving: An Interpolating Theorem Prover (KLM), pp. 16–30.
CAV-2004-AwedhS #bound #model checking: Proving More Properties with Bounded Model Checking (MA, FS), pp. 96–108.
CAV-2004-BallCLZ #abstraction #automation #named #refinement #theorem proving: Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement (TB, BC, SKL, LZ), pp. 457–461.
CSL-2004-GanzingerK #equation #reasoning #theorem proving: Integrating Equational Reasoning into Instantiation-Based Theorem Proving (HG, KK), pp. 71–84.
CSL-2004-GiacobazziM: Proving Abstract Non-interference (RG, IM), pp. 280–294.
CSL-2004-Hyland #abstract interpretation #calculus: Abstract Interpretation of Proofs: Classical Propositional Calculus (MH), pp. 6–21.
CSL-2004-Lynch #theorem proving: Unsound Theorem Proving (CL), pp. 473–487.
CSL-2004-StrassburgerL #linear #logic #multi #on the: On Proof Nets for Multiplicative Linear Logic with Units (LS, FL), pp. 145–159.
IJCAR-2004-DenneyFS #automation #theorem proving #using: Using Automated Theorem Provers to Certify Auto-generated Aerospace Software (ED, BF, JS), pp. 198–212.
IJCAR-2004-GanzingerSW #composition #similarity: Modular Proof Systems for Partial Functions with Weak Equality (HG, VSS, UW), pp. 168–182.
IJCAR-2004-HustadtKRV #named: TeMP: A Temporal Monodic Prover (UH, BK, AR, AV), pp. 326–330.
IJCAR-2004-MengP #interactive #using: Experiments on Supporting Interactive Proof Using Resolution (JM, LCP), pp. 372–384.
IJCAR-2004-ThiemannGS #composition #dependence #termination #using: Improved Modular Termination Proofs Using Dependency Pairs (RT, JG, PSK), pp. 75–90.
IJCAR-2004-WintersteinBG #diagrams #theorem proving: Dr.Doodle: A Diagrammatic Theorem Prover (DW, AB, CAG), pp. 331–335.
LICS-2004-Leivant #logic #termination: Proving Termination Assertions in Dynamic Logics (DL), pp. 89–98.
LICS-2004-Razborov: Feasible Proofs and Computations: Partnership and Fusion (AAR), pp. 134–138.
LICS-2004-Terui: Proof Nets and Boolean Circuits (KT), pp. 182–191.
DRR-2003-ChewB #interactive #named: BaffleText: a human interactive proof (MC, HSB), pp. 305–316.
ICALP-2003-MerroN #bisimulation #mobile: Bisimulation Proof Methods for Mobile Ambients (MM, FZN), pp. 584–598.
FME-2003-Henderson #correctness #using: Proving the Correctness of Simpson’s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method (NH), pp. 244–263.
FME-2003-MammarL #automation #database #design #refinement: Design of an Automatic Prover Dedicated to the Refinement of Database Applications (AM, RL), pp. 834–854.
FME-2003-MillerTH: Proving the Shalls (SPM, ACT, MPEH), pp. 75–93.
FME-2003-RosuELM #equation: Certifying and Synthesizing Membership Equational Proofs (GR, SE, PL, JM), pp. 359–380.
RTA-2003-Kutsia #equation: Equational Prover of THEOREMA (TK), pp. 367–379.
SEFM-2003-DeharbeR #debugging #theorem proving #verification: Light-Weight Theorem Proving for Debugging and Verifying Units of Code (DD, SR), pp. 220–228.
TLCA-2003-Montelatici #fixpoint #semantics: Polarized Proof Nets with Cycles and Fixpoints Semantics (RM), pp. 256–270.
TLCA-2003-Oury #coq #equivalence: Observational Equivalence and Program Extraction in the Coq Proof Assistant (NO), pp. 271–285.
LOPSTR-2003-AlexandreBD #induction #synthesis: Predicate Synthesis from Inductive Proof Attempt of Faulty Conjectures (FA, KB, MD), pp. 20–33.
LOPSTR-2003-LehmannL #generative #induction #theorem proving #using: Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce (HL, ML), pp. 1–19.
LOPSTR-2003-SerebrenikS #termination: Proving Termination with Adornments (AS, DDS), pp. 108–109.
PLDI-2003-LernerMC #automation #compilation #correctness #optimisation: Automatically proving the correctness of compiler optimizations (SL, TDM, CC), pp. 220–231.
PPDP-2003-WuAS: Foundational proof checkers with small witnesses (DW, AWA, AS), pp. 264–274.
ASE-2003-EllisI #automation #exception: Automation for Exception Freedom Proofs (BJE, AI), pp. 343–346.
DATE-2003-GoldbergN #satisfiability #verification: Verification of Proofs of Unsatisfiability for CNF Formulas (EIG, YN), pp. 10886–10891.
ESOP-2003-Ohori: Register Allocation by Proof Transformation (AO), pp. 399–413.
FoSSaCS-2003-SprengerD #calculus #induction #on the #reasoning #μ-calculus: On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μ-Calculus (CS, MD), pp. 425–440.
STOC-2003-Friedman: A proof of Alon’s second eigenvalue conjecture (JF), pp. 720–724.
STOC-2003-KabanetsI #bound #polynomial #testing: Derandomizing polynomial identity tests means proving circuit lower bounds (VK, RI), pp. 355–364.
TACAS-2003-GurfinkelC: Proof-Like Counter-Examples (AG, MC), pp. 160–175.
CADE-2003-DeplagneKKN #equation #induction #theorem: Proof Search and Proof Check for Equational and Inductive Theorems (ED, CK, HK, QHN), pp. 297–316.
CADE-2003-DixonF #named #prototype #theorem proving: IsaPlanner: A Prototype Proof Planner in Isabelle (LD, JDF), pp. 279–283.
CADE-2003-HustadtK: TRP++2.0: A Temporal Resolution Prover (UH, BK), pp. 274–278.
CADE-2003-MehtaN #higher-order #logic #pointer #source code: Proving Pointer Programs in Higher-Order Logic (FM, TN), pp. 121–135.
CADE-2003-Nivelle #axiom #first-order: Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms (HdN), pp. 365–379.
CAV-2003-DongRS #model checking: Evidence Explorer: A Tool for Exploring Model-Checking Proofs (YD, CRR, SAS), pp. 215–218.
CAV-2003-FlanaganJOS #lazy evaluation #theorem proving #using: Theorem Proving Using Lazy Proof Explication (CF, RJ, XO, JBS), pp. 355–367.
CSL-2003-Iemhoff #towards: Towards a Proof System for Admissibility (RI), pp. 255–270.
FATES-2003-HahnleW #testing #theorem proving #using: Using a Software Testing Technique to Improve Theorem Proving (RH, AW), pp. 30–41.
ICLP-2003-BruscoliG #logic programming #tutorial: A Tutorial on Proof Theoretic Foundations of Logic Programming (PB, AG), pp. 109–127.
LICS-2003-GanzingerK #theorem proving: New Directions in Instantiation-Based Theorem Proving (HG, KK), pp. 55–64.
LICS-2003-HughesG #linear #logic #multi: Proof Nets for Unit-free Multiplicative-Additive Linear Logic (DJDH, RJvG), pp. 1–10.
LICS-2003-MillerT: A Proof Theory for Generic Judgments: An extended abstract (DM, AFT), pp. 118–127.
LICS-2003-Oliva #algorithm #effectiveness #polynomial: Polynomial-time Algorithms from Ineffective Proofs (PO), pp. 128–137.
VMCAI-2003-Namjoshi #abstraction: Lifting Temporal Proofs through Abstractions (KSN), pp. 174–188.
ICALP-2002-GrigorievHP #algebra #bound #exponential: Exponential Lower Bound for Static Semi-algebraic Proofs (DG, EAH, DVP), pp. 257–268.
FME-2002-Shankar: Little Engines of Proof (NS), pp. 1–20.
FME-2002-Wildman #compilation: A Formal Basis for a Program Compilation Proof Tool (LW), pp. 491–510.
IFM-2002-BarradasB #liveness #specification: Specification and Proof of Liveness Properties under Fairness Assumptions in B Event Systems (HRB, DB), pp. 360–379.
IFL-2002-DowseSB #haskell: Proving Make Correct: I/O Proofs in Haskell and Clean (MD, GS, AB), pp. 68–83.
ICEIS-2002-ViaeneBDVP #pattern matching #pattern recognition #recognition #state of the art: Proof Running Two State-Of-The-Art Pattern Recognition Techniques in the Field of Direct Marketing (SV, BB, GD, JV, DVdP), pp. 446–454.
LOPSTR-2002-BossiFPR #data flow #security: A Proof System for Information Flow Security (AB, RF, CP, SR), pp. 199–218.
POPL-2002-LaceyJWF #compilation #correctness #logic #optimisation: Proving correctness of compiler optimizations by temporal logic (DL, NDJ, EVW, CCF), pp. 283–294.
PPDP-2002-FissoreGK #induction #termination: System Presentation — CARIBOO: An induction based proof tool for termination with strategies (OF, IG, HK), pp. 62–73.
SAS-2002-VeldhuizenL #compilation #optimisation: Guaranteed Optimization: Proving Nullspace Properties of Compilers (TLV, AL), pp. 263–277.
DAC-2002-AnderssonBCH #approach #automation #design #problem: A proof engine approach to solving combinational design automation problems (GA, PB, BC, ZH), pp. 725–730.
ESOP-2002-WandW #analysis #composition: A Modular, Extensible Proof Method for Small-Step Flow Analyses (MW, GBW), pp. 213–227.
FoSSaCS-2002-BoerGM #concurrent #constraints #correctness #source code: Proving Correctness of Timed Concurrent Constraint Programs (FSdB, MG, MCM), pp. 37–51.
FoSSaCS-2002-JancarKMS #automaton #bound: Equivalence-Checking with One-Counter Automata: A Generic Method for Proving Lower Bounds (PJ, AK, FM, ZS), pp. 172–186.
FoSSaCS-2002-Santocanale #calculus #category theory #semantics: A Calculus of Circular Proofs and Its Categorical Semantics (LS), pp. 357–371.
STOC-2002-DworkS: 2-round zero knowledge and proof auditors (CD, LJS), pp. 322–331.
STOC-2002-DziembowskiM #bound #security: Tight security proofs for the bounded-storage model (SD, UMM), pp. 341–350.
CADE-2002-Baaz #analysis: Proof Analysis by Resolution (MB), pp. 517–532.
CADE-2002-Brown #higher-order #set #theorem proving: Solving for Set Variables in Higher-Order Theorem Proving (CEB), pp. 408–422.
CADE-2002-GalmicheM #logic: Connection-Based Proof Search in Propositional BI Logic (DG, DM), pp. 111–128.
CADE-2002-MouraRS #bound #infinity #lazy evaluation #model checking #theorem proving: Lazy Theorem Proving for Bounded Model Checking over Infinite Domains (LMdM, HR, MS), pp. 438–455.
CADE-2002-SiekmannBBCFFHKMMMNPSUWZ #development: Proof Development with OMEGA (JHS, CB, VB, LC, AF, AF, HH, MK, AM, EM, MM, IN, MP, VS, CU, CPW, JZ), pp. 144–149.
CADE-2002-StumpD #framework #logic #performance: Faster Proof Checking in the Edinburgh Logical Framework (AS, DLD), pp. 392–407.
CAV-2002-BlomP #confluence #reduction: State Space Reduction by Proving Confluence (SB, JvdP), pp. 596–609.
CAV-2002-ColonS #termination: Practical Methods for Proving Program Termination (MC, HS), pp. 442–454.
CAV-2002-HenzingerJMNSW: Temporal-Safety Proofs for Systems Code (TAH, RJ, RM, GCN, GS, WW), pp. 526–538.
CSL-2002-AtseriasB #on the: On the Automatizability of Resolution and Related Propositional Proof Systems (AA, MLB), pp. 569–583.
CSL-2002-Beckmann #strict: Resolution Refutations and Propositional Proofs with Height-Restrictions (AB), pp. 599–612.
CSL-2002-GeuversJ #interactive #logic: Open Proofs and Open Terms: A Basis for Interactive Logic (HG, GIJ), pp. 537–552.
CSL-2002-HodasLPSP #logic programming #resource management: A Tag-Frame System of Resource Management for Proof Search in Linear-Logic Programming (JSH, PL, JP, LS, EP), pp. 167–182.
CSL-2002-Nivelle #normalisation: Extraction of Proofs from the Clausal Normal Form Transformation (HdN), pp. 584–598.
CSL-2002-Ogata #continuation: A Proof Theoretical Account of Continuation Passing Style (IO), pp. 490–505.
ICLP-2002-Bruscoli #logic: A Purely Logical Account of Sequentiality in Proof Search (PB), pp. 302–316.
ICLP-2002-Craciunescu #equivalence #source code: Proving the Equivalence of CLP Programs (SC), pp. 287–301.
LICS-2002-Cook #complexity: Complexity Classes, Propositional Proof Systems, and Formal Theories (SAC), p. 311.
LICS-2002-Shankar: Little Engines of Proof (NS), p. 3–?.
LICS-2002-SoltysC #algebra #complexity #linear: The Proof Complexity of Linear Algebra (MS, SAC), pp. 335–344.
SAT-2002-MotterM #on the #performance #satisfiability: On proof systems behind efficient SAT solvers (DM, IM), p. 31.
TestCom-2002-CastanetR #analysis #reachability #testing #theorem proving: Generate Certified Test Cases by Combining Theorem Proving and Reachability Analysis (RC, DR), pp. 249–266.
VMCAI-2002-FocardiPR #bisimulation #data flow #security: Proofs Methods for Bisimulation Based Information Flow Security (RF, CP, SR), pp. 16–31.
DLT-2001-Razborov #complexity: Proof Complexity of Pigeonhole Principles (AAR), pp. 100–116.
ICALP-2001-GoldreichVW #interactive #on the: On Interactive Proofs with a Laconic Prover (OG, SPV, AW), pp. 334–345.
FME-2001-StoySA #correctness #protocol: Proofs of Correctness of Cache-Coherence Protocols (JES, XS, A), pp. 43–71.
RTA-2001-Barendregt: Computing and Proving (HB), p. 1.
RTA-2001-Hofbauer #termination: Termination Proofs by Context-Dependent Interpretations (DH), pp. 108–121.
RTA-2001-VestergaardB #confluence #first-order #using #λ-calculus: A Formalised First-Order Confluence Proof for the λ-Calculus Using One-Sorted Variable Names (RV, JB), pp. 306–321.
FLOPS-J2-1998-Sakurai01 #category theory: Categorical Model Construction for Proving Syntactic Properties (TS), pp. 213–244.
FLOPS-2001-PolakovY #exception #framework #logic #order: Proving Syntactic Properties of Exceptions in an Ordered Logical Framework (JP, KY), pp. 61–77.
IFL-2001-ButterfieldS #comparison #correctness #paradigm #source code: Proving Correctness of Programs with IO — A Paradigm Comparison (AB, GS), pp. 72–87.
IFL-2001-EncinaP #correctness: Proving the Correctness of the STG Machine (AdlE, RP), pp. 88–104.
IFL-2001-MolEP #functional #theorem proving: Theorem Proving for Functional Programmers (MdM, MCJDvE, MJP), pp. 55–71.
LOPSTR-2001-DelzannoE #debugging #logic programming #protocol #security: Proof Theory, Transformations, and Logic Programming for Debugging Security Protocols (GD, SE), pp. 76–90.
LOPSTR-2001-FerrariFO #bound #logic: Extracting Exact Time Bounds from Logical Proofs (MF, CF, MO), pp. 245–266.
ASE-2001-CookIM #higher-order #synthesis #theorem proving: Higher Order Function Synthesis Through Proof Planning (AC, AI, GM), pp. 307–310.
FASE-2001-InverardiU #component #concurrent #programming: Proving Deadlock Freedom in Component-Based Programming (PI, SU), pp. 60–75.
FoSSaCS-2001-BartheP #dependent type #morphism #reuse #type system: Type Isomorphisms and Proof Reuse in Dependent Type Theory (GB, OP), pp. 57–71.
STOC-2001-AchlioptasBM #complexity: A sharp threshold in proof complexity (DA, PB, MSOM), pp. 337–346.
CAV-2001-Bertot #formal method #theorem proving #verification: Formalizing a JVML Verifier for Initialization in a Theorem Prover (YB), pp. 14–24.
ICLP-2001-DrabentM #approach #correctness #declarative #source code: Proving Correctness and Completeness of Normal Programs — A Declarative Approach (WD, MM), pp. 284–299.
IJCAR-2001-Beeson #higher-order #theorem proving: A Second-Order Theorem Prover Applied to Circumscription (MB), pp. 318–324.
IJCAR-2001-CerroFGHLM #logic: Lotrec : The Generic Tableau Prover for Modal and Description Logics (LFdC, DF, OG, AH, DL, FM), pp. 453–458.
IJCAR-2001-EglyS #composition #source code: Deriving Modular Programs from Short Proofs (UE, SS), pp. 561–577.
IJCAR-2001-Fiedler #interactive: P.rex: An Interactive Proof Explainer (AF), pp. 416–420.
IJCAR-2001-Happe #theorem proving: The MODPROF Theorem Prover (JH), pp. 459–463.
IJCAR-2001-HodasT #agile #first-order #implementation #linear #logic #named #theorem proving: lolliCop — A Linear Logic Implementation of a Lean Connection-Method Theorem Prover for First-Order Classical Logic (JSH, NT), pp. 670–684.
IJCAR-2001-LetzS #calculus #named #theorem proving: DCTP — A Disconnection Calculus Theorem Prover — System Abstract (RL, GS), pp. 381–385.
IJCAR-2001-NieuwenhuisHRV #evaluation #on the #theorem proving: On the Evaluation of Indexing Techniques for Theorem Proving (RN, TH, AR, AV), pp. 257–271.
IJCAR-2001-Pastre #deduction #knowledge-based #theorem proving: MUSCADET 2.3: A Knowledge-Based Theorem Prover Based on Natural Deduction (DP), pp. 685–689.
IJCAR-2001-Paulson #set: SET Cardholder Registration: The Secrecy Proofs (LCP), pp. 5–12.
IJCAR-2001-SchmittLKN #interactive #theorem proving: JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants (SS, LL, CK, AN), pp. 421–426.
IJCAR-2001-Stuber #modelling: A Model-Based Completeness Proof of Extended Narrowing and Resolution (JS), pp. 195–210.
IJCAR-2001-Urbain #automation #incremental #term rewriting #termination: Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems (XU), pp. 485–498.
LICS-2001-Pfenning #type system: Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory (FP), pp. 221–230.
SAT-2001-Goldberg #satisfiability: Proving unsatisfiability of CNFs locally (EG), pp. 96–114.
SAT-2001-McllraithA #theorem proving: Theorem Proving with Structured Theories (Preliminary Report)* (SM, EA), pp. 311–328.
ICALP-2000-AielloBOR #performance #verification: Fast Verification of Any Remote Procedure Call: Short Witness-Indistinguishable One-Round Proofs for NP (WA, SNB, RO, SR), pp. 463–474.
ICALP-2000-AtseriasGG #principle: Monotone Proofs of the Pigeon Hole Principle (AA, NG, RG), pp. 151–162.
ICALP-2000-Moszkowski #logic: An Automata-Theoretic Completeness Proof for Interval Temporal Logic (BCM), pp. 223–234.
ICALP-2000-SantisCP: Necessary and Sufficient Assumptions for Non-iterative Zero-Knowledge Proofs of Knowledge for All NP Relations (ADS, GDC, GP), pp. 451–462.
WLC-2000-Shoji #theorem: A Proof of Okninski, Putcha’s Theorem (KS), pp. 420–427.
UML-2000-Padawitz #constraints #diagrams #how #state machine #theorem proving #uml: Swinging UML: How to Make Class Diagrams and State Machines Amenable to Constraint Solving and Proving (PP), pp. 162–177.
TOOLS-ASIA-2000-WuJZ #design #implementation #normalisation #object-oriented: Implementation and Proof for Normalization Design of Object-Oriented Data Schemes (YW, WJ, AZ), pp. 220–229.
LOPSTR-2000-PoernomoC #protocol #source code: Protocols between programs and proofs (IP, JNC).
LOPSTR-J-2000-PoernomoC #protocol #source code: Protocols between Programs and Proofs (IP, JNC), pp. 18–37.
PPDP-2000-Faggian #calculus #clustering #commutative: Proof construction and non-commutativity: a cluster calculus (CF), pp. 80–91.
PPDP-2000-Gramlich #preprocessor #term rewriting #termination: Simplifying termination proofs for rewrite systems by preprocessing (BG), pp. 139–150.
PPDP-2000-RoychoudhuryRR #using: Justifying proofs using memo tables (AR, CRR, IVR), pp. 178–189.
ICSE-2000-KeidarKLS #incremental #simulation: An inheritance-based technique for building simulation proofs incrementally (IK, RK, NAL, AAS), pp. 478–487.
FoSSaCS-2000-CosmoKP: Proof Nets and Explicit Substitutions (RDC, DK, EP), pp. 63–81.
FoSSaCS-2000-LinY #automaton: A Proof System for Timed Automata (HL, WY), pp. 208–222.
STOC-2000-BihamBBMR #quantum #security: A proof of the security of quantum key distribution (EB, MB, POB, TM, VPR), pp. 715–724.
STOC-2000-CrescenzoSY #on the: On zero-knowledge proofs (extended abstract): “from membership to decision” (GDC, KS, MY), pp. 255–264.
STOC-2000-KitaevW #exponential #interactive #parallel #quantum #simulation: Parallelization, amplification, and exponential time simulation of quantum interactive proof systems (AK, JW), pp. 608–617.
STOC-2000-MacielPW #principle: A new proof of the weak pigeonhole principle (AM, TP, ARW), pp. 368–377.
STOC-2000-Vadhan #complexity #interactive #on the: On transformation of interactive proofs that preserve the prover’s complexity (SPV), pp. 200–207.
TACAS-2000-Aspinall #development: Proof General: A Generic Tool for Proof Development (DA0), pp. 38–42.
TACAS-2000-MeyerP #architecture #interactive: An Architecture for Interactive Program Provers (JM, APH), pp. 63–77.
WRLA-2000-KirchnerG #normalisation #termination: Termination and normalisation under strategy Proofs in ELAN (HK, IG), pp. 93–120.
CADE-2000-AndrewsB #education #higher-order #logic #named #theorem proving #tutorial #using: Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic (PBA, CEB), pp. 511–512.
CADE-2000-AndrewsBB #theorem proving #type system: System Description: TPS: A Theorem Proving System for Type Theory (PBA, MB, CEB), pp. 164–169.
CADE-2000-BezemHN #automation #type system #using: Automated Proof Construction in Type Theory Using Resolution (MB, DH, HdN), pp. 148–163.
CADE-2000-Harrison #theorem proving #using #verification: High-Level Verification Using Theorem Proving and Formalized Mathematics (JH), pp. 1–6.
CADE-2000-JacksonL #interactive: System Description: Interactive Proof Critics in XBarnacle (MJ, HL), pp. 502–506.
CADE-2000-Meier: System Description: TRAMP: Transformation of Machine-Found Proofs into ND-Proofs at the Assertion Level (AM), pp. 460–464.
CADE-2000-NeculaL #generative #theorem proving: Proof Generation in the Touchstone Theorem Prover (GCN, PL), pp. 25–44.
CADE-2000-Seger #float #model checking #theorem proving: Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice (CJHS), p. 235.
CADE-2000-Sinz #algebra #automation #theorem proving: System Description: ARA — An Automatic Theorem Prover for Relation Algebras (CS), pp. 177–182.
CL-2000-HahnleHS #constraints #finite #generative #theorem proving: Moder Generation Theorem Proving with Finite Interval Constraints (RH, RH, YS), pp. 285–299.
CL-2000-HarlandLW #logic #multi: Goal-Directed Proof Search in Multiple-Conclusions Intuitionistic Logic (JH, TL, MW), pp. 254–268.
CL-2000-Lopez-FraguasH #functional #logic programming #source code: Proving Failure in Functional Logic Programs (FJLF, JSH), pp. 179–193.
CL-2000-MelisM #multi #theorem proving: Proof Planning with Multiple Strategies (EM, AM), pp. 644–659.
CSL-2000-BaazZ #fuzzy #logic: Hypersequent and the Proof Theory of Intuitionistic Fuzzy Logic (MB, RZ), pp. 187–201.
CSL-2000-Yavorsky #logic #on the #standard: On the Logic of the Standard Proof Predicate (REY), pp. 527–541.
LICS-2000-McMillan #model checking #theorem: Some Strategies for Proving Theorems with a Model Checker (KLM), pp. 305–306.
LICS-2000-MurawskiO #performance #verification: Dominator Trees and Fast Verification of Proof Nets (ASM, CHLO), pp. 181–191.
LICS-2000-Voronkov #calculus #how #logic: How to Optimize Proof-Search in Modal Logics: A New Way of Proving Redundancy Criteria for Sequent Calculi (AV), pp. 401–412.
ICALP-1999-ComptonD #encryption #protocol: Proof Techniques for Cryptographic Protocols (KJC, SD), pp. 25–39.
ICALP-1999-Miculan #calculus #formal method #induction #lazy evaluation #μ-calculus: Formalizing a Lazy Substitution Proof System for μ-calculus in the Calculus of Inductive Constructions (MM), pp. 554–564.
ICALP-1999-Szegedy #artificial reality #logic: Many-Valued Logics and Holographic Proofs (MS), pp. 676–686.
FM-v1-1999-MoninK #algorithm #consistency #correctness #standard: Correctness Proof of the Standardized Algorithm for ABR Conformance (JFM, FK), pp. 662–681.
FM-v2-1999-KingHCP #experience #industrial #verification: The Value of Verification: Positive Experience of Industrial Proof (SK, JH, RC, AP), pp. 1527–1545.
FM-v2-1999-Moreira #component: Proof Preservation in Component Generalization (AMM), p. 1866.
FM-v2-1999-Nadjm-TehraniA #design #modelling #theorem proving: Combining Theorem Proving and Continuous Models in Synchronous Design (SNT, OÅ), pp. 1384–1399.
FM-v2-1999-RandimbivololonaSBPRS #approach: Applying Formal Proof Techniques to Avionics Software: A Pragmatic Approach (FR, JS, PB, AP, JR, DS), pp. 1798–1815.
IFM-1999-Hennessy #calculus #message passing #process: Proof Systems for Message-Passing Process Calculi (MH), p. 26.
RTA-1999-CosmoG #normalisation: Strong Normalization of Proof Nets Modulo Structural Congruences (RDC, SG), pp. 75–89.
ICFP-1999-Crary #parametricity: A Simple Proof Technique for Certain Parametricity Results (KC), pp. 82–89.
ICFP-1999-ZdancewicGM #programming language: Principals in Programming Languages: A Syntactic Proof Technique (SZ, DG, JGM), pp. 197–207.
AGTIVE-1999-MolE #prototype: A Proof Tool Dedicated to Clean — The First Prototype (MdM, MCJDvE), pp. 271–278.
LOPSTR-1999-DucasseR #consistency #formal method: Proof Obligations of the B Formal Method: Local Proofs Ensure Global Consistency (MD, LR), pp. 10–29.
PADL-1999-Lai #constraints #debugging #using: Using Constraints in Local Proofs for CLP Debugging (CL), pp. 350–359.
PPDP-1999-KamareddineM #on the #recursion #termination: On Formalised Proofs of Termination of Recursive Functions (FK, FM), pp. 29–46.
PPDP-1999-VerbaetenSS #composition #prolog #termination: Modular Termination Proofs for Prolog with Tabling (SV, KFS, DDS), pp. 342–359.
ASE-1999-FedeleK #automation: Automatic Proofs of Properties of Simple C-- Modules (CF, EK), pp. 283–286.
ASE-1999-StarkI #automation #imperative #synthesis #theorem proving #towards: Towards Automatic Imperative Program Synthesis Through Proof Planning (JS, AI), pp. 44–51.
FASE-1999-LuthTKK #development #theorem proving #tool support: TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving (CL, HT, K, BKB), pp. 239–243.
STOC-1999-Ben-SassonW: Short Proofs are Narrow — Resolution Made Simple (EBS, AW), pp. 517–526.
STOC-1999-KlivansM #graph #morphism #polynomial: Graph Nonisomorphism has Subexponential Size Proofs Unless the Polynomial-Time Hierarchy Collapses (AK, DvM), pp. 659–667.
TACAS-1999-HickeyLR #specification: Specifications and Proofs for Ensemble Layers (JH, NAL, RvR), pp. 119–133.
TACAS-1999-Pusch #bytecode #higher-order #java #specification #verification: Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL (CP), pp. 89–103.
TACAS-1999-RusuS #abstraction #on the #safety #static analysis #theorem proving: On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction (VR, ES), pp. 178–192.
CADE-1999-Artemov #on the #theorem proving #verification: On Explicit Reflection in Theorem Proving and Formal Verification (SNA), pp. 267–281.
CADE-1999-FrankeK #automation #communication #distributed #theorem proving: System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving (AF, MK), pp. 217–221.
CADE-1999-Hickey #distributed #fault tolerance #theorem proving: Fault-Tolerant Distributed Theorem Proving (JH), pp. 227–231.
CADE-1999-Horacek: Presenting Proofs in a Human-Oriented Way (HH), pp. 142–156.
CADE-1999-HutterB #contest #design #induction #theorem proving: The Design of the CADE-16 Inductive Theorem Prover Contest (DH, AB), pp. 374–377.
CADE-1999-JanicicBG #flexibility #framework #integration #theorem proving: A Framework for the Flexible Integration of a Class of Decision Procedures into Theorem Provers (PJ, AB, IG), pp. 127–141.
CADE-1999-Lopes #automation #generative #higher-order #logic: Automatic Generation of Proof Search Strategies for Second-order Logic (RHCL), pp. 414–428.
CADE-1999-Nipkow #programming language #theorem proving: Invited Talk: Embedding Programming Languages in Theorem Provers (TN), p. 398.
CADE-1999-Voronkov #named #theorem proving: KK: a theorem prover for K (AV), pp. 383–387.
CAV-1999-GlusmanK #equivalence: Mechanizing Proofs of Computation Equivalence (MG, SK), pp. 354–367.
CAV-1999-ManoliosNS #bisimulation #model checking #theorem proving: Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation (PM, KSN, RS), pp. 369–379.
CSL-1999-GeuversPZ #type system: Safe Proof Checking in Type Theory with Y (HG, EP, JZ), pp. 439–452.
CSL-1999-Howe #interactive #theorem proving #type system #using: Interactive Theorem Proving Using Type Theory (DJH), p. 578.
CSL-1999-Roversi #logic: A P-Time Completeness Proof for Light Logics (LR), pp. 469–483.
ICLP-1999-Smaus #logic programming #source code #termination: Proving Termination of Input-Consuming Logic Programs (JGS), pp. 335–349.
LICS-1999-BorealeNP #encryption #process: Proof Techniques for Cryptographic Processes (MB, RDN, RP), pp. 157–166.
LICS-1999-Guerrini #correctness #linear #multi: Correctness of Multiplicative Proof Nets Is Linear (SG), pp. 454–463.
LICS-1999-Paulson #protocol #security: Proving Security Protocols Correct (LCP), pp. 370–381.
CSMR-1998-JakobiW #automation #database #evaluation #framework #maintenance #named #theorem proving: DBFW: A Simple DataBase FrameWork for the Evaluation and Maintenance of Automated Theorem Prover Data (PJ, AW), pp. 185–188.
ICALP-1998-GrafV: Reducing Simple Polygons to Triangles — A Proof for an Improved Conjecture (TG, KV), pp. 130–139.
ICALP-1998-Lin #π-calculus: Complete Proof Systems for Observation Congruences in Finite-Control π-Calculus (HL), pp. 443–454.
ICALP-1998-Lugiez #automaton #induction #theorem proving: A Good Class of Tree Automata and Application to Inductive Theorem Proving (DL), pp. 409–420.
WIA-1998-LHerPM #automaton #source code #using: Proving Sequential Function Chart Programs Using Automata (DL, PLP, LM), pp. 149–163.
RTA-1998-Comon #consistency: About Proofs by Consistency (HC), pp. 136–137.
RTA-1998-Fuchs #information management: Coupling Saturation-Based Provers by Exchanging Positive/Negative Information (DF), pp. 317–331.
RTA-1998-Xi #automation #termination #towards: Towards Automated Termination Proofs through “Freezing” (HX), pp. 271–285.
FLOPS-1998-Sakurai: Categorial Model Construction for Proving Syntactic Properties (TS), pp. 187–206.
ECOOP-1998-FerreiraS #algorithm #correctness #distributed #garbage collection #modelling: Modelling a Distributed Cached Store for Garbage Collection: The Algorithm and Its Correctness Proof (PF, MS), pp. 234–259.
ALP-PLILP-1998-LeviV #abstract interpretation: Derivation of Proof Methods by Abstract Interpretation (GL, PV), pp. 102–117.
LOPSTR-1998-Richardson #named #theorem proving: Abstract: Proof Planning with Program Schemas (JR), pp. 313–315.
LOPSTR-1998-StarkI #invariant: Invariant Discovery via Failed Proof Attempts (JS, AI), pp. 271–288.
POPL-1998-Blanchet #analysis #correctness #implementation: Escape Analysis: Correctness Proof, Implementation and Experimental Results (BB), pp. 25–37.
ASE-1998-Ledru #identification #theorem proving: Identifying Pre-Conditions with the Z/EVES Theorem Prover (YL), p. 32–?.
FSE-1998-FongC #architecture #composition #mobile #verification: Proof Linking: An Architecture for Modular Verification of Dynamically-Linked Mobile Code (PWLF, RDC), pp. 222–230.
DAC-1998-AagaardJS #evaluation #industrial #theorem proving: Combining Theorem Proving and Trajectory Evaluation in an Industrial Environment (MA, RBJ, CJHS), pp. 538–541.
FASE-1998-BerregebBR: Observational Proofs with Critical Contexts (NB, AB, MR), pp. 38–53.
STOC-1998-BeameKPS #complexity #on the #random #satisfiability: On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas (PB, RMK, TP, MES), pp. 561–571.
TACAS-1998-JensenL #abstraction #algorithm #using: A Proof of Burns N-Process Mutual Exclusion Algorithm Using Abstraction (HEJ, NAL), pp. 409–423.
CADE-1998-BenzmullerK98a #higher-order #theorem proving: System Description: LEO — A Higher-Order Theorem Prover (CB, MK), pp. 139–144.
CADE-1998-FeveW #algebra #geometry #theorem #using: Proving Geometric Theorems Using Clifford Algebra and Rewrite Rules (SF, DW), pp. 17–31.
CADE-1998-FleuriotP #analysis #geometry #standard #theorem proving: A Combination of Nonstandard Analysis and Geometry Theorem Proving, with Application to Newton’s Principia (JDF, LCP), pp. 3–16.
CADE-1998-GorePSV #smarttech #theorem proving: System Description: card TAP: The First Theorem Prover on a Smart Card (RG, JP, AS, HV), pp. 47–50.
CADE-1998-KreitzHH #communication #development: A Proof Environment for the Development of Group Communication Systems (CK, MH, JH), pp. 317–332.
CADE-1998-RichardsonSG #higher-order #logic #theorem proving: System Description: Proof Planning in Higher-Order Logic with Lambda-Clam (JR, AS, IG), pp. 129–133.
CADE-1998-SchurmannP #automation #logic #theorem proving: Automated Theorem Proving in a Simple Meta-Logic for LF (CS, FP), pp. 286–300.
CAV-1998-Camilleri #design #multi #theorem proving: A Role for Theorem Proving in Multi-Processor Design (AJC), pp. 45–48.
CAV-1998-HardinWG #concept #design #theorem proving: Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle (DSH, MW, DAG), pp. 39–44.
CAV-1998-HosabettuSG #correctness #pipes and filters: Decomposing the Proof of Correctness of pipelined Microprocessors (RH, MKS, GG), pp. 122–134.
CAV-1998-Moore: An ACL2 Proof of Write Invalidate Cache Coherence (JSM), pp. 29–38.
CAV-1998-Wilding #policy #realtime #scheduling: A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy (MW), pp. 369–378.
LICS-1998-JohannsenP #on the: On Proofs about Threshold Circuits and Counting Hierarchies (JJ, CP), pp. 444–452.
LICS-1998-NeculaL #performance #representation #validation: Efficient Representation and Validation of Proofs (GCN, PL), pp. 93–104.
ICALP-1997-Fu #approach #communication: A Proof Theoretical Approach to Communication (YF), pp. 325–335.
FME-1997-AgerholmF #automation #theorem proving #towards: Towards an Integrated CASE and Theorem Proving Tool for VDM-SL (SA, JF), pp. 278–297.
FME-1997-AichernigL #generative: A Proof Obligation Generator for VDM-SL (BKA, PGL), pp. 338–357.
FME-1997-BoerHR #composition #concurrent: A Compositional Proof System for Shared Variable Concurrency (FSdB, UH, WPdR), pp. 515–532.
FME-1997-Gregoire #protocol #using: TLA + PROMELA: Conjecture, Check, Proof, Engineering New Protocols Using Methods and Formal Notations (JCG), pp. 378–397.
RTA-1997-ArtsG #automation #normalisation: Proving Innermost Normalisation Automatically (TA, JG), pp. 157–171.
RTA-1997-KapurS #order #term rewriting #termination: A Total, Ground path Ordering for Proving Termination of AC-Rewrite Systems (DK, GS), pp. 142–156.
RTA-1997-KuhlerW #data type #equation #induction #specification #theorem proving: Conditional Equational Specifications of Data Types with Partial Operations for Inductive Theorem Proving (UK, CPW), pp. 38–52.
TLCA-1997-GuerriniMM: Proof Nets, Garbage, and Computations (SG, SM, AM), pp. 181–195.
TLCA-1997-Ruess #calculus #theorem proving: Computational Reflection in the Calculus of Constructions and its Application to Theorem Proving (HR), pp. 319–335.
ALP-1997-CairesM #semantics: Proof Net Semantics of Proof Search Computation (LC, LM), pp. 194–208.
POPL-1997-Sands #functional: From SOS Rules to Proof Principles: An Operational Metatheory for Functional Languages (DS), pp. 428–441.
SAS-1997-PanitzS #automation #functional #higher-order #named #source code #strict #termination: TEA: Automatically Proving Termination of Programs in a Non-strict Higher-Order Functional Language (SEP, MSS), pp. 345–360.
STOC-1997-CramerD #linear #performance: Linear Zero-Knowledge — A Note on Efficient Zero-Knowledge Proofs and Arguments (RC, ID), pp. 436–445.
STOC-1997-KilianPT: Probabilistically Checkable Proofs with Zero Knowledge (JK, EP, GT), pp. 496–505.
STOC-1997-MacielP #on the: On ACC0[pk] Frege Proofs (AM, TP), pp. 720–729.
STOC-1997-Mulmuley #algebra #exclamation #question: Is There an Algebraic Proof for P != NC? (KM), pp. 210–219.
STOC-1997-RazborovWY #branch #calculus #source code: Read-Once Branching Programs, Rectangular Proofs of the Pigeonhole Principle and the Transversal Calculus (AAR, AW, ACCY), pp. 739–748.
TACAS-1997-SandnerM #refinement #theorem proving: Theorem Prover Support for the Refinement of Stream Processing Functions (RS, OM), pp. 351–365.
TAPSOFT-1997-ArtsG #automation #order #termination: Automatically Proving Termination Where Simplification Orderings Fail (TA, JG), pp. 261–272.
TAPSOFT-1997-BouhoulaJM #equation #logic #specification: Specification and Proof in Membership Equational Logic (AB, JPJ, JM), pp. 67–92.
TAPSOFT-1997-GenetG #constraints #termination #using: Termination Proofs Using gpo Ordering Constraints (TG, IG), pp. 249–260.
TAPSOFT-1997-Jacobs #algebra #behaviour #correctness #induction #specification: Behaviour-Refinement of Coalgebraic Specifications with Coinductive Correctness Proofs (BJ0), pp. 787–802.
TAPSOFT-1997-KolyangLMW #development #interface #theorem proving: TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving (K0, CL, TM0, BW), pp. 855–858.
TAPSOFT-1997-KristoffersenLLPY #composition #protocol #realtime: A Compositional Proof of a Real-Time Mutual Exclusion Protocol (KJK, FL, KGL, PP, WY0), pp. 565–579.
TAPSOFT-1997-Lenisa #induction #λ-calculus: A Uniform Syntactical Method for Proving Coinduction Principles in Lambda-Calculi (ML), pp. 309–320.
TAPSOFT-1997-ReifSS #correctness: Proving System Correctness with KIV (WR, GS, KS), pp. 859–862.
TAPSOFT-1997-Voisin #interface: A new Proof-Manager and Graphic Interface for the Larch Prover (FV), pp. 863–866.
CADE-1997-Bonacina #theorem proving: The Clause-Diffusion Theorem Prover Peers-mcd (MPB), pp. 53–56.
CADE-1997-DahnGHW #automation #integration #interactive #theorem proving: Integration of Automated and Interactive Theorem Proving in ILP (BID, JG, TH, AW), pp. 57–60.
CADE-1997-DefourneauxP: Partial Matching for Analogy Discovery in Proofs and Counter-Examples (GD, NP), pp. 431–445.
CADE-1997-DennisBG #bisimulation #induction #using: Using A Generalisation Critic to Find Bisimulations for Coinductive Proofs (LAD, AB, IG), pp. 276–290.
CADE-1997-EastaughffeOC #formal method #state machine #visual notation: Proof Tactics for a Theory of State Machines in a Graphical Environment (KAE, MAO, AC), pp. 366–379.
CADE-1997-FeltyH #hybrid #interactive #theorem proving #using: Hybrid Interactive Theorem Proving Using Nuprl and HOL (APF, DJH), pp. 351–365.
CADE-1997-FuchsF #named #problem: CODE: A Powerful Prover for Problems of Condensed Detachment (DF, MF), pp. 260–263.
CADE-1997-HasegawaIOK #bottom-up #set #theorem proving #top-down: Non-Horn Magic Sets to Incorporate Top-down Inference into Bottom-up Theorem Proving (RH, KI, YO, MK), pp. 176–190.
CADE-1997-Iwanuma #theorem proving #top-down: Lemma Matching for a PTTP-based Top-down Theorem Prover (KI), pp. 146–160.
CADE-1997-KolbeB #learning #named: Plagiator — A Learning Prover (TK, JB), pp. 256–259.
CADE-1997-KreitzMOS #linear #logic: Connection-Based Proof Construction in Linear Logic (CK, HM, JO, SS), pp. 207–221.
CADE-1997-LoweD #named #theorem proving: XBarnacle: Making Theorem Provers More Accessible (HL, DD), pp. 404–407.
CADE-1997-OheimbG #algebra #named: RALL: Machine-Supported Proofs for Relation Algebra (DvO, TFG), pp. 380–394.
CADE-1997-ReifSS #correctness: Proving System Correctness with KIV 3.0 (WR, GS, KS), pp. 69–72.
CADE-1997-Slaney #logic #named #theorem proving: Minlog: A Minimal Logic Theorem Prover (JKS), pp. 268–271.
CADE-1997-WolfS #named #natural language: ILF-SETHEO: Processing Model Elimination Proofs for Natural Language Output (AW, JS), pp. 61–64.
CADE-1997-Zhang #named #performance: SATO: An Efficient Propositional Prover (HZ), pp. 272–275.
CSL-1997-Faggian #logic: Classical Proofs via Basic Logic (CF), pp. 203–219.
LICS-1997-CosmoK #normalisation: Strong Normalization of Explicit Substitutions via Cut Elimination in Proof Nets (RDC, DK), pp. 35–46.
ICALP-1996-Ganzinger #theorem proving: Saturation-Based Theorem Proving (HG), pp. 1–3.
ICALP-1996-Razborov #bound #independence: Lower Bounds for Propositional Proofs and Independence Results in Bounded Arithmetic (AAR), pp. 48–62.
FME-1996-HavelundS #model checking #protocol #theorem proving #verification: Experiments in Theorem Proving and Model Checking for Protocol Verification (KH, NS), pp. 662–681.
FME-1996-Hoare #how #question #reliability: How Did Software Get So Reliable Without Proof? (CARH), pp. 1–17.
RTA-1996-BerregebBR #commutative #induction #named: SPIKE-AC: A System for Proofs by Induction in Associative-Commutative Theories (NB, AB, MR), pp. 428–431.
RTA-1996-BoudetCM #theorem proving #unification: AC-Complete Unification and its Application to Theorem Proving (AB, EC, CM), pp. 18–32.
RTA-1996-Gramlich #on the #termination: On Proving Termination by Innermost Termination (BG), pp. 93–107.
RTA-1996-GuerriniMM: Coherence for Sharing Proof Nets (SG, SM, AM), pp. 215–229.
RTA-1996-HillenbrandBF #on the #performance #theorem proving: On Gaining Efficiency in Completion-Based Theorem Proving (TH, AB, RF), pp. 432–435.
RTA-1996-Huet #design: Design Proof Assistant (GPH), p. 153.
RTA-1996-Luth #algebra #composition #term rewriting #theorem: Compositional Term Rewriting: An Algebraic Proof of Toyama’s Theorem (CL), pp. 261–275.
RTA-1996-Stuber #integer #theorem proving: Superposition Theorem Proving for Albelian Groups Represented as Integer Modules (JS), pp. 33–47.
RTA-1996-VandevoordeK #distributed #empirical #rule-based: Distributed Larch Prover (DLP): An Experiment in Parallelizing a Rewrite-Rule Based Prover (MTV, DK), pp. 420–423.
RTA-1996-Voisin #interface: A New Proof Manager and Graphic Interface for Larch Prover (FV), pp. 408–411.
ALP-1996-Volpe #abstraction: Abstractions of Uniform Proofs (PV), pp. 224–237.
LOPSTR-1996-DungKT #reasoning #synthesis: Synthesis of Proof Procedures for Default Reasoning (PMD, RAK, FT), pp. 313–324.
POPL-1996-HughesPS #correctness #using: Proving the Correctness of Reactive Systems Using Sized Types (JH, LP, AS), pp. 410–423.
SAS-1996-BoerGP #constraints #correctness #logic programming #scheduling #source code: Proving Correctness of Constraint Logic Programs with Dynamic Scheduling (FSdB, MG, CP), pp. 83–97.
SAS-1996-MullerGS #automation #composition #prolog #source code #termination: Automated Modular Termination Proofs for Real Prolog Programs (MM, TG, KS), pp. 220–237.
ICSE-1996-Hoare #how #question #reliability: The Role of Formal Techniques: Past, Current and Future or How Did Software Get so Reliable without Proof? (CARH), pp. 233–234.
TAPSOFT-J-1995-Sands96 #automation #correctness #program transformation #recursion: Proving the Correctness of Recursion-Based Automatic Program Transformations (DS), pp. 193–233.
STOC-1996-CleggEI #algorithm #satisfiability #using: Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability (MC, JE, RI), pp. 174–183.
STOC-1996-Fu #composition: Modular Coloring Formulas Are Hard for Cutting Planes Proofs (XF), pp. 595–602.
STOC-1996-Okamoto #on the #statistics: On Relationships between Statistical Zero-Knowledge Proofs (TO), pp. 649–658.
TACAS-1996-Lamport: Managing Proofs (LL), p. 34.
TACAS-1996-Saidi #automation #concurrent: A Tool for Proving Invariance Properties of Concurrent Systems Automatically (HS), pp. 412–416.
CADE-1996-BeckertHOS #theorem proving: The Tableau-based Theorem Prover 3TAP Version 4.0 (BB, RH, PO, MS), pp. 303–307.
CADE-1996-DenzingerS #learning #theorem proving: Learning Domain Knowledge to Improve Theorem Proving (JD, SS), pp. 62–76.
CADE-1996-Felty #calculus #set: Proof Search with Set Variable Instantiation in the Calculus of Constructions (APF), pp. 658–672.
CADE-1996-Fuchs #experience #heuristic #using: Experiments in the Heuristic Use of Past Proof Experience (MF), pp. 523–537.
CADE-1996-Ganzinger #theorem proving: Saturation-Based Theorem Proving: Past Successes and Future Potential (HG), p. 1.
CADE-1996-GanzingerW #monad #theorem proving: Theorem Proving in Cancellative Abelian Monoids (HG, UW), pp. 388–402.
CADE-1996-GiunchigliaV #abstraction #named: ABSFOL: A Proof Checker with Abstraction (FG, AV), pp. 136–140.
CADE-1996-Harrison #optimisation: Optimizing Proof Search in Model Elimination (JH), pp. 313–327.
CADE-1996-HuangF: Presenting Machine-Found Proofs (XH, AF), pp. 221–225.
CADE-1996-IrelandB #induction: Extensions to a Generalization Critic for Inductive Proof (AI, AB), pp. 47–61.
CADE-1996-KolbeW #reuse #termination #theorem proving: Termination of Theorem Proving by Reuse (TK, CW), pp. 106–120.
CADE-1996-Luz-Filho #logic #specification #theorem proving: Grammar Specification in Categorial Logics and Theorem Proving (SFLF), pp. 703–717.
CADE-1996-Martin #theorem proving: Theorem Proving with Group Presentations: Examples and Questions (UM), pp. 358–372.
CADE-1996-MelisW #theorem proving: Internal Analogy in Theorem Proving (EM, JW), pp. 92–105.
CADE-1996-Nipkow #higher-order: More Church-Rosser Proofs (in Isabelle/HOL) (TN), pp. 733–747.
CADE-1996-SchaubBN #named #prolog #reasoning #theorem proving: XRay: A Prolog Technology Theorem Prover for Default Reasoning: A System Description (TS, SB, PN), pp. 293–297.
CADE-1996-SchmittK #matrix: Converting Non-Classical Matrix Proofs into Sequent-Style Systems (SS, CK), pp. 418–432.
CADE-1996-Schumann #named #parallel #theorem proving: SiCoTHEO: Simple Competitive Parallel Theorem Provers (JS), pp. 240–244.
CADE-1996-Tammet #logic #theorem proving: A Resolution Theorem Prover for Intuitonistic Logic (TT), pp. 2–16.
CADE-1996-Wang #geometry #named #theorem proving: GEOTHER: A Geometry Theorem Prover (DW), pp. 166–170.
CAV-1996-ClarkeGZ #algorithm #theorem proving #using #verification: Verifying the SRT Division Algorithm Using Theorem Proving Techniques (EMC, SMG, XZ), pp. 111–122.
CAV-1996-GrafS #invariant #theorem proving #using #verification: Verifying Invariants Using theorem Proving (SG, HS), pp. 196–207.
CAV-1996-OwreRRSS #model checking #named #specification: PVS: Combining Specification, Proof Checking, and Model Checking (SO, SR, JMR, NS, MKS), pp. 411–414.
CSL-1996-Malecki: Proofs in System Fω Can Be Done in System Fω¹ (SM), pp. 297–315.
JICSLP-1996-Thielscher #logic programming #semantics #source code: A Nonmonotonic Disputation-Based Semantics and Proof Procedure for Logic Programs (MT), pp. 483–497.
LICS-1996-Ong #category theory #semantics: A Semantic View of Classical Proofs: Type-Theoretic, Categorical, and Denotational Characterizations (CHLO), pp. 230–241.
FPLE-1995-HartelET #student: Basic Proof Skills of Computer Science Students (PHH, BvE, DT), pp. 269–287.
RTA-1995-Giesl #generative #order #polynomial #termination: Generating Polynomial Orderings for Termination Proofs (JG), pp. 426–431.
RTA-1995-Holmes #equation #recursion #theorem: Disguising Recursively Chained Rewrite Rules as Equational Theorems, as Implemented in the Prover EFTTP Mark 2 (MRH), pp. 432–437.
RTA-1995-Kahrs #termination #towards: Towards a Domain Theory for Termination Proofs (SK), pp. 241–255.
RTA-1995-Kuper #reduction: Proving the Genericity Lemma by Leftmost Reduction is Simple (JK), pp. 271–278.
RTA-1995-Nieuwenhuis #constraints #on the: On Narrowing, Refutation Proofs and Constraints (RN), pp. 56–70.
RTA-1995-Steinbach #automation #order #termination: Automatic Termination Proofs With Transformation Orderings (JS), pp. 11–25.
RTA-1995-Stickel #term rewriting #theorem proving: Term Rewriting in Contemporary Resolution Theorem Proving (MES), p. 101.
TLCA-1995-CoscoyKT: Extracting Text from Proofs (YC, GK, LT), pp. 109–123.
TLCA-1995-Leclerc #coq #development #multi #order #term rewriting #termination: Termination Proof of Term Rewriting System with the Multiset Path Ordering. A Complete Development in the System Coq (FL), pp. 312–327.
TLCA-1995-PolS #strict #termination: Strict Functionals for Termination Proofs (JvdP, HS), pp. 350–364.
ICML-1995-Fuchs #adaptation #heuristic #learning #parametricity: Learning Proof Heuristics by Adaptive Parameters (MF), pp. 235–243.
LOPSTR-1995-KreitzOS #development: Guiding Program Development Systems by a Connection Based Proof Strategy (CK, JO, SS), pp. 137–151.
LOPSTR-1995-Renault #logic programming #source code #towards: Towards a Complete Proof Procedure to Prove Properties of Normal Logic Programs under the Completion (SR), pp. 204–218.
PEPM-1995-Metayer #data type #recursion #source code: Proving Properties of Programs Defined over Recursive Data Structures (DLM), pp. 88–99.
ESEC-1995-Coen-PorisiniKM #framework: A Formal Framework for ASTRAL Inter-level Proof Obligations (ACP, RAK, DM), pp. 90–108.
SAC-1995-Bsaies #logic programming: Discovering and proving logic program properties (KB), pp. 369–373.
ASF+SDF-1995-NaidichD #asf+sdf #automation #induction #specification: Specifying an Automated Induction Proof Procedure in ASF+SDF (DN, TBD), pp. 233–254.
STOC-1995-BonetPR #bound: Lower bounds for cutting planes proofs with small coefficients (MLB, TP, RR), pp. 575–584.
STOC-1995-FeigeK #random: Impossibility results for recycling random bits in two-prover proof systems (UF, JK), pp. 457–468.
TACAS-1995-LarsenSW #constraints: A Constraint Oriented Proof Methodology Based on Modal Transition Systems (KGL, BS, CW), pp. 17–40.
TAPSOFT-1995-Geser #induction: Mechanized Inductive Proof of Properties of a Simple Code Optimizer (AG), pp. 605–619.
TAPSOFT-1995-MannaBBCCADKLSU #named: STeP: The Stanford Temporal Prover (ZM, NB, AB, EYC, MC, LdA, HD, AK, JL, HS, TEU), pp. 793–794.
TAPSOFT-1995-SampaioHPUFA #named #programming #term rewriting: PLATO: A Tool to Assist Programming as Term Rewriting and Therem Proving (AJS, AMH, CTP, CDU, MFF, NCA), pp. 797–798.
TAPSOFT-1995-Sands #automation #correctness #program transformation #recursion: Proving the Correctness of Recursion-Based Automatic Program Transformations (DS), pp. 681–695.
CAV-1995-DingelF #abstraction #infinity #model checking #reasoning #theorem proving #using: Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving (JD, TF), pp. 54–69.
CAV-1995-RajanSS #automation #integration #model checking: An Integration of Model Checking with Automated Proof Checking (SR, NS, MKS), pp. 84–97.
ICLP-1995-FormicaMT #database #object-oriented #satisfiability #theorem proving: A Theorem Prover for Checking Satisfiability of Object-Oriented Database Schemas (AF, MM, RT), p. 819.
ICLP-1995-Hasegawa #generative #theorem proving: Model Generation Theorem Provers and Their Applications (RH), p. 7.
ICLP-1995-Hirata #correctness #haskell #π-calculus: Proving Correctness of Translation from Moded Flat GHC to π-Calculus (KH), p. 818.
ILPS-1995-FerrandL #composition #correctness #logic programming #source code: A Compositional Proof Method of Partial Correctness for Normal Logic Programs (GF, AL), pp. 209–223.
ILPS-1995-Hui-Bon-Hoa: Clause-based proofs for hereditary Harrop formulas (AHBH), pp. 179–193.
ILPS-1995-MarchioriT #logic programming #source code #termination: Proving Termination of Logic Programs with Delay Declarations (EM, FT), pp. 447–461.
LICS-1995-Dutertre #first-order #logic: Complete Proof Systems for First Order Interval Temporal Logic (BD), pp. 36–43.
LICS-1995-KestenP: A Complete Proof Systems for QPTL (YK, AP), pp. 2–12.
LICS-1995-KfouryW #normalisation #reduction #semantics #λ-calculus: New Notions of Reduction and Non-Semantic Proofs of β-Strong Normalization in Typed λ-Calculi (AJK, JBW), pp. 311–321.
LICS-1995-NadathurL #logic programming: Uniform Proofs and Disjunctive Logic Programming (GN, DWL), pp. 148–155.
LFP-1994-Cosmadakis #algebra: Complete Proof Systems for Algebraic Simply-Typed Terms (SSC), pp. 220–226.
KR-1994-AttardiS: Proofs in Context (GA, MS), pp. 15–26.
ALP-1994-BidoitH #behaviour #first-order #logic #standard #theorem: Proving Behavioural Theorems with Standard First-Order Logic (MB, RH), pp. 41–58.
ALP-1994-Bouhoula #induction: Sufficient Completeness and Parameterized Proofs by Induction (AB), pp. 23–40.
ALP-1994-CodishM #algebra #approximate: Proving Implications by Algebraic Approximation (MC, GM), pp. 6–22.
ALP-1994-Volpe #concurrent #linear #logic programming: Concurrent Logic Programming as Uniform Linear Proofs (PV), pp. 133–149.
LOPSTR-1994-AttardiS: Building Proofs in Context (GA, MS), pp. 410–424.
POPL-1994-BoerGMP #concurrent #constraints #source code: Proving Concurrent Constraint Programs Correct (FSdB, MG, EM, CP), pp. 98–108.
ESOP-J-1992-Henglein94 #dynamic typing #syntax #type system: Dynamic Typing: Syntax and Proof Theory (FH), pp. 197–230.
ESOP-1994-Walker #algebra: Algebraic Proofs of Properties of Objects (DW), pp. 501–516.
STOC-1994-BellareGLR #approximate #performance #probability: Efficient probabilistic checkable proofs and applications to approximation (MB, SG, CL, AR), p. 820.
STOC-1994-FeigeK #fault #protocol: Two prover protocols: low error at affordable rates (UF, JK), pp. 172–183.
STOC-1994-PolishchukS #artificial reality: Nearly-linear size holographic proofs (AP, DAS), pp. 194–203.
STOC-1994-RazborovR: Natural proofs (AAR, SR), pp. 204–213.
CADE-1994-Anderson #optimisation #representation: Representing Proof Transformations for Program Optimizations (PA), pp. 575–589.
CADE-1994-BaumgartnerF94a #interface #named: PROTEIN: A PROver with a Theory Extension INterface (PB, UF), pp. 769–773.
CADE-1994-BeckertP #agile #named #theorem proving: leanTAP: Lean Tableau-Based Theorem Proving (BB, JP), pp. 793–797.
CADE-1994-BonacinaM #distributed #theorem proving: Distributed Theorem Proving by Peers (MPB, WM), pp. 841–845.
CADE-1994-Bouhoula #induction #named: SPIKE: a System for Sufficient Completeness and Parameterized Inductive Proofs (AB), pp. 836–840.
CADE-1994-ChazarainK #induction: Mechanizable Inductive Proofs for a Class of Forall Exists Formulas (JC, EK), pp. 118–132.
CADE-1994-ChuP #first-order #semantics #theorem proving #using: Semantically Guided First-Order Theorem Proving using Hyper-Linking (HC, DAP), pp. 192–206.
CADE-1994-ClarkeZ #problem #symbolic computation #theorem proving: Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan (EMC, XZ), pp. 758–763.
CADE-1994-FarmerGNT: Proof Script Pragmatics in IMPS (WMF, JDG, MEN, FJT), pp. 356–370.
CADE-1994-FeltyH #theorem proving: Tactic Theorem Proving with Refinement-Tree Proofs and Metavariables (APF, DJH), pp. 605–619.
CADE-1994-Goubault: Proving with BDDs and Control of Information (JG), pp. 499–513.
CADE-1994-Huang #re-engineering: Reconstruction Proofs at the Assertion Level (XH), pp. 738–752.
CADE-1994-HuangKKMNRS #development #named: Omega-MKRP: A Proof Development Environment (XH, MK, MK, EM, DN, JR, JHS), pp. 788–792.
CADE-1994-Hutter #induction #order #synthesis: Synthesis of Induction Orderings for Existence Proofs (DH), pp. 29–41.
CADE-1994-Lysne #consistency #on the: On the Connection between Narrowing and Proof by Consistency (OL), pp. 133–147.
CADE-1994-McPheeCG #geometry #theorem #using: Mechanically Proving Geometry Theorems Using a Combination of Wu’s Method and Collins’ Method (NFM, SCC, XSG), pp. 401–415.
CADE-1994-Plaisted #performance #theorem proving: The Search Efficiency of Theorem Proving Strategies (DAP), pp. 57–71.
CADE-1994-Platek #question #what: What is a Proof? (RP), p. 431.
CADE-1994-Portoraro #automation #named: Symlog: Automated Advice in Fitch-style Proof Construction (FDP), pp. 802–806.
CADE-1994-Schumann #bottom-up #named #preprocessor #theorem proving #top-down: DELTA — A Bottom-up Preprocessor for Top-Down Theorem Provers — System Abstract (JS), pp. 774–777.
CADE-1994-WaalG #logic programming #program analysis #program transformation #theorem proving: The Applicability of Logic Program Analysis and Transformation to Theorem Proving (DAdW, JPG), pp. 207–221.
CADE-1994-Wang #algebra #geometry: Algebraic Factoring and Geometry Proving (DW), pp. 386–400.
ICLP-1994-BreuerSK #design #hardware: Proving Hardware Designs (PTB, LS, CDK), p. 745.
ICLP-1994-Pedreschi #prolog #runtime #source code: A Proof Method for Runtime Properties of Prolog Programs (DP), pp. 584–598.
LICS-1994-AndersenSW #calculus #composition #μ-calculus: A Compositional Proof System for the Modal μ-Calculus (HRA, CS, GW), pp. 144–153.
LICS-1994-BaazFL: A Non-Elementary Speed-Up in Proof Length by Structural Clause Form Transformation (MB, CGF, AL), pp. 213–219.
LICS-1994-Burstall #refinement: Terms, Proofs, and Refinement (RMB), pp. 2–7.
LICS-1994-HofmannS: The Groupoid Model Refutes Uniqueness of Identity Proofs (MH, TS), pp. 208–212.
LICS-1994-ImpagliazzoPU #bound: Upper and Lower Bounds for Tree-Like Cutting Planes Proofs (RI, TP, AU), pp. 220–228.
LICS-1994-LincolnS #calculus #first-order #linear #logic: Proof Search in First-Order Linear Logic and Other Cut-Free Sequent Calculi (PL, NS), pp. 282–291.
FME-1993-BrownM #concurrent #source code: A Proof Environment for Concurrent Programs (NB, DM), pp. 196–215.
RTA-1993-AvenhausD #equation #theorem proving: Distributing Equational Theorem Proving (JA, JD), pp. 62–76.
RTA-1993-Bachmair #theorem proving: Rewrite Techniques in Theorem Proving (LB), p. 1.
RTA-1993-Gallier: Proving Properties of Typed λ Terms: Realizability, Covers, and Sheaves (JHG), p. 136.
TLCA-1993-Altenkirch #formal method #normalisation #system f: A Formalization of the Strong Normalization Proof for System F in LEGO (TA), pp. 13–28.
TLCA-1993-Berger #normalisation: Program Extraction from Normalization Proofs (UB0), pp. 91–106.
TLCA-1993-HylandO #normalisation: Modified Realizability Toposes and Strong Normalization Proofs (JMEH, CHLO), pp. 179–194.
LOPSTR-1993-LombartWD #synthesis: Guiding Synthesis Proofs (VL, GAW, YD), pp. 67–81.
LOPSTR-1993-MaddenHGB #automation #generative #performance #source code #theorem proving #using: A General Technique for Automatically Generating Efficient Programs Through the Use of Proof Planning (PM, JH, IG, AB), pp. 64–66.
LOPSTR-1993-ProiettiP #source code #synthesis: Synthesis of Programs from Unfold/Fold Proofs (MP, AP), pp. 141–158.
PEPM-1993-Lawall #induction #partial evaluation #using: Proofs by Structural Induction using Partial Evaluation (JLL), pp. 155–166.
PLILP-1993-BurnM #analysis #compilation #correctness #optimisation #strict: Proving the Correctness of Compiler Optimizations Based on Strictness Analysis (GLB, DLM), pp. 346–364.
ESEC-1993-Coen-PorisiniM #framework: A Formal Framework for ASTRAL Intra-Level Proof Obligations (ACP, DM), pp. 483–500.
PDP-1993-BettazM #concurrent #modelling: Modelling and proving of truly concurrent systems with CATNets (MB, AM), pp. 265–272.
STOC-1993-BellareGLR #approximate #performance: Efficient probabilistically checkable proofs and applications to approximations (MB, SG, CL, AR), pp. 294–304.
STOC-1993-CoffmanJSW #analysis #markov: Markov chains, computer proofs, and average-case analysis of best fit bin packing (EGCJ, DSJ, PWS, RRW), pp. 412–421.
TAPSOFT-1993-Becker #confluence #equation #induction #specification: Proving Ground Confluence and Inductive Validity in Constructor Based Equational Specifications (KB0), pp. 46–60.
CAV-1993-Hungar #model checking #parallel #process #theorem proving #verification: Combining Model Checking and Theorem Proving to Verify Parallel Processes (HH), pp. 154–165.
CAV-1993-Sogaard-AndersenGGLP #simulation: Computer-Assisted Simulation Proofs (JFSA, SJG, JVG, NAL, AP), pp. 305–319.
CSL-1993-BaazZ #equivalence #using: Short Proofs of Tautologies Using the Schema of Equivalence (MB, RZ), pp. 33–35.
CSL-1993-SiegW #program transformation: Program Transformation and Proof Transformation (WS, SSW), pp. 305–317.
ICLP-1993-McCarty #higher-order #induction #logic #prolog #source code: Proving Inductive Properties of Prolog Programs in Second-Order Intuitionistic Logic (LTM), pp. 44–63.
ICLP-1993-RaoKS #haskell #source code #termination: Proving Termination of GHC Programs (MRKKR, DK, RKS), pp. 720–736.
ILPS-1993-BarbackL: A Proof Procedure for Default Theories with Extensions (MDB, JL), p. 651.
ILPS-1993-KirschenbaumS #prolog #source code: Enhancement Structures for Proving Prolog Programs Correct (MK, LS), p. 631.
ILPS-1993-Teusink #logic programming #source code: A Proof Procedure for Extended Logic Programs (FT), pp. 235–249.
ICALP-1992-SantisPY #bound #statistics #verification: One-Message Statistical Zero-Knowledge Proofs and Space-Bounded Verifier (ADS, GP, MY), pp. 28–40.
LFP-1992-ChirimarGR #invariant #linear #logic #memory management: Proving Memory Management Invariants for a Language Based on Linear Logic (JC, CAG, JGR), pp. 139–150.
LFP-1992-WandO #correctness: Proving the Correctness of Storage Representations (MW, DO), pp. 151–160.
KR-1992-Lamarre #theorem proving: A Promenade from Monotonicity to Non-Monotonicity Following a Theorem Prover (PL), pp. 572–580.
SEKE-1992-KaoH #graph #logic #realtime: A Graph Proof Procedure for Real Time Logic (JHK, LJH), pp. 300–306.
ALP-1992-BachmairGW #first-order #theorem proving: Theorem Proving for Hierarchic First-Order Theories (LB, HG, UW), pp. 420–434.
ALP-1992-Lysne #algebra #consistency #semantics: Proof by Consistency in Constructive Systems with Final Algebra Semantics (OL), pp. 276–290.
LOPSTR-1992-KraanBB #logic programming #synthesis #theorem proving: Logic Program Synthesis via Proof Planning (IK, DAB, AB), pp. 1–14.
LOPSTR-1992-Ornaghi: Proof Nets (MO), pp. 61–79.
ESOP-1992-BernsteinRS #safety: Proving Safety of Speculative Load Instructions at Compile Time (DB, MR, SS), pp. 56–72.
ESOP-1992-Gnaedig #specification #theorem proving: ELIOS-OBJ Theorem Proving in a Specification Language (IG), pp. 182–199.
STOC-1992-BellareP #performance: Making Zero-Knowledge Provers Efficient (MB, EP), pp. 711–722.
STOC-1992-DorT #composition #graph: Graph Decomposition Is NPC-A Complete Proof of Holyer’s Conjecture (DD, MT), pp. 252–263.
STOC-1992-FeigeL92a #problem: Two-Prover One-Round Proof Systems: Their Power and Their Problems (UF, LL), pp. 733–744.
STOC-1992-Kilian #performance: A Note on Efficient Zero-Knowledge Proofs and Arguments (JK), pp. 723–732.
CADE-1992-AlexanderP #similarity #theorem: Proving Equality Theorems with Hyper-Linking (GDA, DAP), pp. 706–710.
CADE-1992-Ammon #analysis #automation #logic: Automatic Proofs in Mathematical Logic and Analysis (KA), pp. 4–19.
CADE-1992-AstrachanS #theorem proving: Caching and Lemmaizing in Model Elimination Theorem Provers (OLA, MES), pp. 224–238.
CADE-1992-Baker-PlummerR #theorem proving: The GAZER Theorem Prover (DBP, AR), pp. 726–730.
CADE-1992-BeckertGHK #logic #multi #theorem proving: The Tableau-Based Theorem Prover 3TAP for Multi-Valued Logics (BB, SG, RH, WK), pp. 758–760.
CADE-1992-BoyerY #automation #correctness #source code: Automated Correctness Proofs of Machine Code Programs for a Commercial Microprocessor (RSB, YY), pp. 416–430.
CADE-1992-CaferraD #logic #semantics: Semantic Entailment in Non Classical Logics Based on Proofs Found in Classical Logic (RC, SD), pp. 385–399.
CADE-1992-Chen #empirical #knowledge-based #theorem proving: Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic (WZC), pp. 552–566.
CADE-1992-ChirimarGI #interface #named #performance #visual notation: Xpnet: A Graphical Interface to Proof Nets with an Efficient Proof Checker (JC, CAG, MVI), pp. 711–715.
CADE-1992-Chou #geometry #theorem proving: A Geometry Theorem Prover for Macintoshes (SCC), pp. 686–690.
CADE-1992-ChouG #geometry: Proving Geometry Statements of Constructive Type (SCC, XSG), pp. 20–34.
CADE-1992-ClarkeZ #named #theorem proving: Analytica — A Theorem Prover in Mathematica (EMC, XZ), pp. 761–765.
CADE-1992-Dafa #automation #deduction #theorem proving: A Natural Deduction Automated Theorem Proving System (LD), pp. 668–672.
CADE-1992-HasegawaKF #generative #lazy evaluation #named #parallel #theorem proving: MGTP: A Parallel Theorem Prover Based on Lazy Model Generation (RH, MK, HF), pp. 776–780.
CADE-1992-InoueKH #generative #theorem proving: Embedding Negation as Failure into a Model Generation Theorem Prover (KI, MK, RH), pp. 400–415.
CADE-1992-LuskMS #named #parallel #theorem proving: ROO: A Parallel Theorem Prover (ELL, WM, JKS), pp. 731–734.
CADE-1992-Madden #automation #optimisation: Automatic Program Optimization Through Proof Transformation (PM), pp. 446–460.
CADE-1992-NieuwenhuisR #theorem proving: Theorem Proving with Ordering Constrained Clauses (RN, AR), pp. 477–491.
CADE-1992-RandellCC #automation #challenge #theorem proving: Computing Transivity Tables: A Challenge For Automated Theorem Provers (DAR, AGC, ZC), pp. 786–790.
CADE-1992-SchneiderKK: The FAUST — Prover (KS, RK, TK), pp. 766–770.
CADE-1992-Schumann #logic #named #theorem proving: KPROP — An AND-parallel Theorem Prover for Propositional Logic implemented in KL1 (JS), pp. 740–742.
CADE-1992-Shankar #calculus: Proof Search in the Intuitionistic Sequent Calculus (NS), pp. 522–536.
CADE-1992-UribeFM #automation #framework #overview: An Overview of FRAPPS 2.0: A Framework for Resolution-based Automated Proof Procedure Systems (TEU, AMF, MKM), pp. 721–725.
CADE-1992-Voronkov #logic #standard #theorem proving: Theorem Proving in Non-Standard Logics Based on the Inverse Method (AV), pp. 648–662.
CADE-1992-WalshNB #theorem proving #using: The Use of Proof Plans to Sum Series (TW, AN, AB), pp. 325–339.
CADE-1992-ZhangH #induction #set #theorem: Proving the Chinese Remainder Theorem by the Cover Set Induction (HZ, XH), pp. 431–445.
CAV-1992-Bradfield #model checking: A Proof Assistant for Symbolic Model-Checking (JCB), pp. 316–329.
CAV-1992-WrightL #algorithm #concurrent #reasoning #theorem proving #using: Using a Theorem Prover for Reasoning about Concurrent Algorithms (JvW, TL), pp. 56–68.
CSL-1992-ArtemovS #logic: The Basic Logic of Proofs (SNA, TS), pp. 14–28.
CSL-1992-BaazZ #algorithm: Algorithmic Structuring of Cut-free Proofs (MB, RZ), pp. 29–42.
CSL-1992-Creignou #linear #problem #satisfiability: The Class of Problems that are Linear Equivalent to Satisfiability or a Uniform Method for Proving NP-Completeness (NC), pp. 115–133.
JICSLP-1992-BronsardLR #framework #logic programming #source code #termination: A Framework of Directionality for Proving Termination of Logic Programs (FB, TKL, USR), pp. 321–335.
JICSLP-1992-FerrandD #correctness #logic programming #source code: Proof Method of Partial Correctness and Weak Completeness for Normal Logic Programs (GF, PD), pp. 161–174.
JICSLP-1992-GrogerP #automation #logic programming #recursion #source code #termination: Handling of Mutual Recursion in Automatic Termination Proofs for Logic Programs (GG, LP), pp. 336–350.
JICSLP-1992-Wiggins #development #logic programming #source code #synthesis: Synthesis and Transformation of Logic Programs in the Whelk Proof Development System (GAW), pp. 351–365.
LICS-1992-Clote #constant: Cutting Planes and constant depth Frege proofs (PC), pp. 296–307.
RTA-1991-AgarwalMKN: The Tecton Proof System (RA, DRM, DK, XN), pp. 442–444.
RTA-1991-Avenhaus #equation #induction #theorem: Proving Equational and Inductive Theorems by Completion and Embedding Techniques (JA), pp. 361–373.
RTA-1991-BonacinaH #on the #theorem proving: On Fairness of Completion-Based Theorem Proving Strategies (MPB, JH), pp. 348–360.
RTA-1991-Deruyver #equation #first-order #logic #named #theorem proving: EMMY: A Refutational Theorem Prover for First-Order Logic with Equation (AD), pp. 439–441.
RTA-1991-DrewesL #incremental #termination: Incremental Termination Proofs and the Length of Derivations (FD, CL), pp. 49–61.
RTA-1991-Fraus #theorem proving: A Narrowing-Based Theorem Prover (UF), pp. 435–436.
RTA-1991-Hermann #on the: On Proving Properties of Completion Strategies (MH), pp. 398–410.
RTA-1991-Hofbauer #bound #term rewriting #termination: Time Bounded Rewrite Systems and Termination Proofs by Generalized Embedding (DH), pp. 62–73.
RTA-1991-Kirchner #specification: Proofs in Parameterized Specification (HK), pp. 174–187.
VDME-1991-Arthan #on the #specification: On Formal Specification of a Proof Tool (RDA), pp. 356–370.
FPCA-1991-Mairson #parametricity: Outline of a Proof Theory of Parametricity (HGM), pp. 313–327.
KR-1991-HalpernV #model checking #theorem proving: Model Checking vs. Theorem Proving: A Manifesto (JYH, MYV), pp. 325–334.
LOPSTR-1991-WigginsBKH #induction #logic programming #source code #synthesis: Synthesis and Transfomation of Logic Programs from Constructive, Inductive Proof (GAW, AB, IK, JH), pp. 27–45.
PLILP-1991-FrausH #theorem proving: A Narrowing-Based Theorem Prover (UF, HH), pp. 421–422.
POPL-1991-HenzingerMP #realtime: Temporal Proof Methodologies for Real-time Systems (TAH, ZM, AP), pp. 353–366.
CAAP-1991-Ortega-MallenF: A Complete Proof System for Timed Observations (YOM, DdFE), pp. 412–440.
CCPSD-1991-BossiCF #logic programming #source code #termination: Proving Termination of Logic Programs by Exploiting Term Properties (AB, NC, MF), pp. 153–180.
STOC-1991-CoffmanG #scheduling: Proof of the 4/3 Conjecture for Preemptive vs. Nonpreemptive Two-Processor Scheduling (EGCJ, MRG), pp. 241–248.
CAV-1991-BevierS #kernel #specification: Mechanically Checked Proofs of Kernel Specification (WRB, JFSA), pp. 70–82.
CAV-1991-MaoM #automation #equivalence #finite #state machine: An Automated Proof Technique for Finite-State Machine Equivalence (WM, GJM), pp. 233–243.
CAV-1991-MauwV: A Proof Assistant for PSF (SM, GJV), pp. 158–168.
CAV-1991-Mutz #behaviour #correctness #term rewriting #using: Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior (MM), pp. 277–287.
CAV-1991-Nesi #higher-order #induction #logic #process #specification: Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic (MN), pp. 288–298.
CAV-1991-SchneiderKK #automation #hardware: Automating Most Parts of Hardware Proofs in HOL (KS, RK, TK), pp. 365–375.
CSL-1991-BeierleB #correctness: Correctness Proof For the WAM with Types (CB, EB), pp. 15–34.
CSL-1991-Goerdt #bound: The Cutting Plane Proof System with Bounded Degree of Falsity (AG), pp. 119–133.
CSL-1991-RaoKS #logic programming #source code #termination: A Transformational Methodology for Proving Termination of Logic Programs (MRKKR, DK, RKS), pp. 213–226.
CSL-1991-Schmerl #source code: A Cut-Elimination Procedure Designed for Evaluating Proofs as Programs (URS), pp. 316–325.
CSL-1991-Schwichtenberg: Minimal from Classical Proofs (HS), pp. 326–328.
CSL-1991-Weiermann #term rewriting #termination: Proving Termination for Term Rewriting Systems (AW), pp. 419–428.
ICLP-1991-ColussiM #axiom #correctness #logic programming #semantics #source code #using: Proving Correctness of Logic Programs Using Axiomatic Semantics (LC, EM), pp. 629–642.
ICLP-1991-FujitaH #algorithm #generative #theorem proving #using: A Model Generation Theorem Prover in KL1 Using a Ramified -Stack Algorithm (HF, RH), pp. 535–548.
ICLP-1991-Hagiya #higher-order #theorem proving #unification: Higher-Order Unification as a Theorem Proving Procedure (MH), pp. 270–284.
ICLP-1991-Lever: Proving Program Properties by Means of SLS-Resolution (JML), pp. 614–628.
ICLP-1991-VerschaetseS #logic programming #source code #termination #using: Deriving Termination Proofs for Logic Programs, Using Abstract Procedures (KV, DDS), pp. 301–315.
ISLP-1991-Fribourg #automation #generative #induction: Automatic Generation of Simplification Lemmas for Inductive Proofs (LF), pp. 103–116.
ISLP-1991-Nakayama #principle #program transformation: Program Transformation under the Principle of Proof as Program (HN), pp. 626–640.
ISLP-1991-Plumer #automation #prolog #source code #termination: Automatic Termination Proofs for Prolog Programs Operating on Nonground Terms (LP), pp. 503–517.
LICS-1991-Boer #composition #process: A Compositional Proof System for Dynamic Process Creation (FSdB), pp. 399–405.
LICS-1991-BonetB #deduction #on the: On the Deduction Rule and the Number of Proof Lines (MLB, SRB), pp. 286–297.
LICS-1991-Hungar #bound #complexity #hoare: Complexity Bounds of Hoare-style Proof Systems (HH), pp. 120–126.
LICS-1991-HuttelS #process #similarity #word: Actions Speak Louder than Words: Proving Bisimilarity for Context-Free Processes (HH, CS), pp. 376–386.
LICS-1991-Murthy #evaluation #semantics: An Evaluation Semantics for Classical Proofs (CRM), pp. 96–107.
LICS-1991-PeledKP #logic #specification: Specifying and Proving Serializability in Temporal Logic (DP, SK, AP), pp. 232–244.
ICALP-1990-Boer #object-oriented #parallel: A Proof System for the Parallel Object-Oriented Language POOL (FSdB), pp. 572–585.
ICALP-1990-GoldreichK #composition #on the: On the Composition of Zero-Knowledge Proof Systems (OG, HK), pp. 268–282.
ICALP-1990-PeledP #liveness #partial order: Proving Partial Order Liveness Properties (DP, AP), pp. 553–571.
ICALP-1990-Riecke #call-by #decidability: A Complete and Decidable Proof System for Call-by-Value Equalities (JGR), pp. 20–31.
ML-1990-Kodratoff #abduction #problem #using: Using Abductive Recovery of Failed Proofs for Problem Solving by Analogy (YK), pp. 295–303.
ALP-1990-Farres-Casals #correctness #specification: Proving Correctness wrt Specifications with Hidden Parts (JFC), pp. 25–39.
ALP-1990-Goguen: Proving and Rewriting (JAG), pp. 1–24.
ALP-1990-Hofbauer #multi #order #recursion #termination: Termination Proofs by Multiset Path Orderings Imply Primitive Recursive Derivation Lengths (DH), pp. 347–358.
POPL-1990-AspertiFG: Implicative Formulae in the “Proofs as Computations” Analogy (AA, GLF, RG), pp. 59–71.
ICSE-1990-LafontaineLS #case study #development #empirical #formal method #theorem proving #using: An Experiment in Formal Software Development: Using the B Theorem Prover on a VDM Case Study (CL, YL, PYS), pp. 34–42.
DAC-1990-NiermannCP #fault #memory management #named #performance: Proofs: A Fast, Memory Efficient Sequential Circuit Fault Simulator (TMN, WTC, JHP), pp. 535–540.
CADE-1990-AltucherP #category theory: A Mechanically Assisted Constructive Proof in Category Theory (JAA, PP), pp. 500–513.
CADE-1990-AndrewsINP #theorem proving: The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 641–642.
CADE-1990-BoyerM #logic #theorem proving: A Theorem Prover for a Computational Logic (RSB, JSM), pp. 1–15.
CADE-1990-BundyHSI #induction: Extensions to the Rippling-Out Tactic for Guiding Inductive Proofs (AB, FvH, AS, AI), pp. 132–146.
CADE-1990-ButlerFJO #parallel #theorem proving: A High-Performance Parallel Theorem Prover (RB, ITF, AJ, RAO), pp. 649–650.
CADE-1990-ChouG #algorithm #composition #geometry #theorem proving: Ritt-Wu’s Decomposition Algorithm and Geometry Theorem Proving (SCC, XSG), pp. 207–220.
CADE-1990-CostaHLS #automation #implementation #logic #theorem proving: Automatic Theorem Proving in Paraconsistent Logics: Theory and Implementation (NCAdC, LJH, JJL, VSS), pp. 72–86.
CADE-1990-EichenlaubEHKP: The Romulus Proof Checker (CE, BE, JH, CK, GP), pp. 651–652.
CADE-1990-FarmerGT #interactive #named: IMPS: An Interactive Mathematical Proof System (WMF, JDG, FJT), pp. 653–654.
CADE-1990-Gramlich #induction #named #theorem proving: UNICOM: A Refined Completion Based Inductive Theorem Prover (BG), pp. 655–656.
CADE-1990-Hagiya #higher-order #programming #unification #using: Programming by Example and Proving by Example Using Higher-order Unification (MH), pp. 588–602.
CADE-1990-HeiselRS #theorem proving #verification: Tactical Theorem Proving in Program Verification (MH, WR, WS), pp. 117–131.
CADE-1990-Hines #set: Str+ve-Subset: The Str+ve-based Subset Prover (LMH), pp. 193–206.
CADE-1990-HsiangJ #theorem proving #tutorial: Tutorial on Rewrite-Based Theorem Proving (JH, JPJ), p. 684.
CADE-1990-Hutter #induction: Guiding Induction Proofs (DH), pp. 147–161.
CADE-1990-KaflZ #theorem proving #verification: The Theorem Prover of the Program Verifier Tatzelwurm (TK, NZ), pp. 657–658.
CADE-1990-LuskM #automation #theorem proving #tutorial: Tutorial on High-Performance Automated Theorem Proving (ELL, WM), p. 681.
CADE-1990-MurrayR #named #theorem proving: DISSOLVER: A Dissolution-based Theorem Prover (NVM, ER), pp. 665–666.
CADE-1990-NieP #semantics: A Complete Semantic Back Chaining Proof System (XN, DAP), pp. 16–27.
CADE-1990-Pierce #towards: Toward Mechanical Methods for Streamlining Proofs (WP), pp. 351–365.
CADE-1990-SchumannL #named #parallel #theorem proving: PARTHEO: A High-Performance Parallel Theorem Prover (JS, RL), pp. 40–56.
CADE-1990-SchumannLK #implementation #parallel #performance #theorem proving #tutorial: Tutorial on High-Performance Theorem Provers: Efficient Implementation and Parallelisation (JS, RL, FJK), p. 683.
CADE-1990-Schwind #decidability #logic #set #theorem proving: A Tableau-Based Theorem Prover for a Decidable Subset of Default Logic (CS), pp. 528–542.
CADE-1990-Stickel #prolog #theorem proving: A Prolog Technology Theorem Prover (MES), pp. 673–674.
CADE-1990-Sutcliffe #theorem proving: A General Clause Theorem Prover (GS), pp. 675–676.
CADE-1990-Tuominen #framework #logic #theorem proving: Dynamic Logic as a Uniform Framework for Theorem Proving in Intensional Logic (HT), pp. 514–527.
CAV-1990-BuyM #liveness: A Proof Lattice-Based Technique for Analyzing Liveness of Resource Controllers (UAB, RM), pp. 292–301.
CLP-1990-Fribourg90 #execution #induction #logic programming #prolog #source code: Extracting Logic Programs from Proofs that Use Extended Prolog Execution and Induction (LF), pp. 685–699.
CLP-1990-Plumer90 #logic programming #source code #termination: Termination Proofs for Logic Programs Based on Predicate Inequalities (LP), pp. 634–648.
CLP-1990-SawamuraMYO90 #approach #logic #logic programming #specification: A Logic Programming Approach to Specifying Logics and Constructing Proofs (HS, TM, KY, KO), pp. 405–424.
CSL-1990-Gabbay #algorithm: Algorithmic Proof with Diminishing Resources, Part 1 (DMG), pp. 156–173.
CSL-1990-Goerdt: Cuting Plane Versus Frege Proof Systems (AG), pp. 174–194.
CSL-1990-Hahnle #logic #multi #performance #towards: Towards an Efficient Tableau Proof Procedure for Multiple-Valued Logics (RH), pp. 248–260.
CSL-1990-HertrampfW #bound #fault #interactive: Interactive Proof Systems: Provers, Rounds, and Error Bounds (UH, KWW), pp. 261–273.
LICS-1990-AllenCHA #semantics: The Semantics of Reflected Proof (SFA, RLC, DJH, WEA), pp. 95–105.
LICS-1990-CleavelandS #specification #using: When is “Partial” Adequate? A Logic-Based Proof Technique Using Partial Specifications (RC, BS), pp. 440–449.
LICS-1990-MurthyR: A Constructive Proof of Higman’s Lemma (CRM, JRR), pp. 257–267.
LICS-1990-Nipkow #equation: Proof Transformations for Equational Theories (TN), pp. 278–288.
NACLP-1990-Spencer: Avoiding Duplicate Proofs (BS), pp. 569–584.
RTA-1989-AvenhausDM #named #performance #theorem proving: THEOPOGLES — An efficient Theorem Prover based on Rewrite-Techniques (JA, JD, JM), pp. 538–541.
RTA-1989-Bachmair #normalisation: Proof Normalization for Resolution and Paramodulation (LB), pp. 15–28.
RTA-1989-BonacinaS #equation #named #theorem proving: KBlab: An Equational Theorem Prover for the Macintosh (MPB, GS), pp. 548–550.
RTA-1989-Comon #induction #specification: Inductive Proofs by Specification Transformation (HC), pp. 76–91.
RTA-1989-HofbauerL #termination: Termination Proofs and the Length of Derivations (DH, CL), pp. 167–177.
FPCA-1989-Takayama #performance #source code: Extended Projection — New Method to Extract Efficient Programs from Constructive Proofs (YT), pp. 299–312.
SEKE-1989-Cooke #design: Proving Properties of Software Design Methods (DEC), pp. 9–12.
POPL-1989-Paulin-Mohring #calculus #source code: Extracting Fω’s Programs from Proofs in the Calculus of Constructions (CPM), pp. 89–104.
CAAP-1989-Deransart #declarative #logic programming #source code: Proofs of Declarative Properties of Logic Programs (PD), pp. 207–226.
CAAP-1989-Padawitz #induction: Inductive Proofs by Resolution and Paramodulation (PP), pp. 352–368.
STOC-1989-Birget: Proof of a Conjecture of R. Kannan (JCB), pp. 445–453.
CSL-1989-Ohlbach #first-order #logic #multi: New Ways for Developing Proof Theories for First-Order Multi Modal Logics (HJO), pp. 271–308.
CSL-1989-Stark: A Direct Proof for the Completeness of SLD-Resolution (RFS), pp. 382–383.
LICS-1989-BoseCLM #horn clause #named #parallel #theorem proving: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (SB, EMC, DEL, SM), pp. 80–89.
LICS-1989-GaifmanS #logic programming #semantics #source code: Proof Theory and Semantics of Logic Programs (HG, EYS), pp. 50–62.
SIGMOD-1988-MazumdarSS #security #theorem proving #using: Resolving the Tension between Integrity and Security Using a Theorem Prover (SM, DWS, TS), pp. 233–242.
ICALP-1988-Culik #decidability #equivalence #problem: New Techniques for Proving the Decidability of Equivalence Problems (KCI), pp. 162–175.
VDME-1988-ButhB #code generation #correctness #specification #term rewriting #using: Correctness Proofs for Meta IV Written Code Generator Specification using Term Rewriting (BB, KHB), pp. 406–433.
VDME-1988-JonesM #design #empirical #named #theorem proving #user interface: MUFFIN: A User Interface Design Experiment for a Theorem Proving Assistant (CBJ, RCM), pp. 337–375.
VDME-1988-Milne: Proof Rules for VDM Statements (RM), pp. 318–336.
ALP-1988-HofbauerK #induction #term rewriting #theorem: Proving Inductive Theorems Based on Term Rewriting Systems (DH, RDK), pp. 180–190.
ALP-1988-Kucherov #algorithm #induction #testing: A New Quasi-Reducibility Testing Algorithm and its Application to Proofs by Induction (GK), pp. 204–213.
DAC-1988-MadreB #behaviour #comparison #correctness #using: Proving Circuit Correctness Using Formal Comparison Between Expected and Extracted Behaviour (JCM, JPB), pp. 205–210.
ESOP-1988-Parigot #higher-order #programming #type system: Programming with Proofs: A Second Order Type Theory (MP), pp. 145–159.
ESOP-1988-Takayama #analysis #compilation #named: QPC: QJ-based Proof Compiler — Simple Examples and Analysis (YT), pp. 49–63.
STOC-1988-Ben-OrGKW #how #interactive #multi: Multi-Prover Interactive Proofs: How to Remove Intractability Assumptions (MBO, SG, JK, AW), pp. 113–131.
CADE-1988-AllenBCM #horn clause #named #parallel #theorem proving: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (PEA, SB, EMC, SM), pp. 764–765.
CADE-1988-AndrewsINP #theorem proving: The TPS Theorem Proving System (PBA, SI, DN, FP), pp. 760–761.
CADE-1988-BrockCP #reasoning: Analogical Reasoning and Proof Discovery (BB, SC, WP), pp. 454–468.
CADE-1988-BrownP #logic #named #theorem proving: SYMEVAL: A Theorem Prover Based on the Experimental Logic (FMB, SSP), pp. 756–757.
CADE-1988-Bundy #induction #using: The Use of Explicit Plans to Guide Inductive Proofs (AB), pp. 111–120.
CADE-1988-CyrlukHK #algebra #geometry #named #theorem proving: GEOMETER: A Theorem Prover for Algebraic Geometry (DC, RMH, DK), pp. 770–771.
CADE-1988-DuchierM #development #interactive #named: LOGICALC: An Environment for Interactive Proof Development (DD, DVM), pp. 121–130.
CADE-1988-FeltyM #higher-order #logic programming #programming language #specification #theorem proving: Specifying Theorem Provers in a Higher-Order Logic Programming Language (APF, DM), pp. 61–80.
CADE-1988-GarlandG #named: LP: The Larch Prover (SJG, JVG), pp. 748–749.
CADE-1988-Hines #knowledge-based #theorem proving: Hyper-Chaining and Knowledge-Based Theorem Proving (LMH), pp. 469–486.
CADE-1988-Kaufmann #interactive #theorem proving: An Interactive Enhancement to the Boyer-Moore Theorem Prover (MK), pp. 735–736.
CADE-1988-MantheyB #named #prolog #theorem proving: SATCHMO: A Theorem Prover Implemented in Prolog (RM, FB), pp. 415–434.
CADE-1988-MarcusR #automation #implementation: Two Automated Methods in Implementation Proofs (LM, TR), pp. 622–642.
CADE-1988-McRobbieMT #automation #knowledge-based #logic #performance #standard #theorem proving #towards: Towards Efficient “Knowledge-Based” Automated Theorem Proving for Non-Standard Logics (MAM, RKM, PBT), pp. 197–217.
CADE-1988-Paulson #named #theorem proving: Isabelle: The Next Seven Hundred Theorem Provers (LCP), pp. 772–773.
CADE-1988-Plaisted #theorem proving: A Goal Directed Theorem Prover (DAP), p. 737.
CADE-1988-Simon #natural language: Checking Natural Language Proofs (DS), pp. 141–150.
CADE-1988-Stevens #challenge #problem #theorem proving: Challenge Problems from Nonassociative Rings for Theorem Provers (RLS), pp. 730–734.
CADE-1988-Stickel88a #prolog #theorem proving: A Prolog Technology Theorem Prover (MES), pp. 752–753.
CADE-1988-Walther #algorithm #automation #bound #termination: Argument-Bounded Algorithms as a Basis for Automated Termination Proofs (CW), pp. 602–621.
CADE-1988-ZhangK #first-order #theorem proving #using: First-Order Theorem Proving Using Conditional Rewrite Rules (HZ, DK), pp. 1–20.
CSL-1988-Plumer #automation #prolog #source code #termination: Predicate Inequalities as a Basis for Automated Termination Proofs for Prolog Programs (LP), pp. 254–271.
JICSCP-1988-BruffaertsH88 #prolog: Proof Trees for Negation as Failure: Yet Another Prolog Meta-Interpreter (AB, EH), pp. 343–358.
LICS-1988-Bachmair #consistency #equation: Proof by Consistency in Equational Theories (LB), pp. 228–233.
LICS-1988-Baudinet #approach #prolog #semantics #source code #termination: Proving Termination Properties of Prolog Programs: A Semantic Approach (MB), pp. 336–347.
LICS-1988-Tiomkin: Proving unprovability (MLT), pp. 22–26.
LICS-1988-Winskel #composition #petri net: A Category of Labelled Petri Nets and Compositional Proof System (GW), pp. 142–154.
VDME-1987-Jones87a: VDM Proof Obligations and their Justification (CBJ), pp. 260–286.
POPL-1987-WidomGS #network: Completeness and Incompleteness of Trace-Based Network Proof Systems (JW, DG, FBS), pp. 27–38.
AS-1987-Milner: Dialogue with a Proof System (RM), pp. 271–275.
CAAP-1987-NavarroO #correctness #horn clause #specification: Parameterized Horn Clause Specifications: Proof Theory and Correctness (MN, FO), pp. 202–216.
STOC-1987-FeigeFS: Zero Knowledge Proofs of Identity (UF, AF, AS), pp. 210–217.
CSL-1987-BryM #database #deduction #finite #satisfiability: Proving Finite Satisfiability of Deductive Databases (FB, RM), pp. 44–55.
ICLP-1987-Vieille87: A Database-Complete Proof Procedure Based on SLD-Resolution (LV), pp. 74–103.
LICS-1987-Abadi #power of: The Power of Temporal Proofs (MA), pp. 123–130.
LICS-1987-AlpernS: Proving Boolean Combinations of Deterministic Properties (BA, FBS), pp. 131–137.
LICS-1987-BachmairD #first-order #theorem proving: Inference Rules for Rewrite-Based First-Order Theorem Proving (LB, ND), pp. 331–337.
LICS-1987-GallierRS #equation #theorem proving #using: Theorem Proving Using Rigid E-Unification Equational Matings (JHG, SR, WS), pp. 338–346.
LICS-1987-MillerNS: Hereditary Harrop Formulas and Uniform Proof Systems (DM, GN, AS), pp. 98–105.
SLP-1987-Takayama87 #compilation #prolog #source code: Writing Programs as QJ Proof and Compiling into Prolog Programs (YT), pp. 278–287.
ESOP-1986-Kaplan #algebra #nondeterminism: Rewriting with a Nondeterministic Choice Operator: From Algebra to Proofs (SK), pp. 351–374.
ESOP-1986-Stark #concept #specification: Proving Entailment Between Conceptual State Specifications (EWS), pp. 197–209.
STOC-1986-GoldwasserS #interactive: Private Coins versus Public Coins in Interactive Proof Systems (SG, MS), pp. 59–68.
CADE-1986-AbadiM #theorem proving: Modal Theorem Proving (MA, ZM), pp. 172–189.
CADE-1986-AndrewsPIK #theorem proving: The TPS Theorem Proving System (PBA, FP, SI, CPK), pp. 663–664.
CADE-1986-BeierleOV #automation #theorem proving: Automatic Theorem Proving in the ISDV System (CB, WGO, AV), pp. 670–671.
CADE-1986-BiundoHHW #induction #theorem proving: The Karlsruhe Induction Theorem Proving System (SB, BH, DH, CW), pp. 672–674.
CADE-1986-ButlerLMO #automation #theorem proving: Paths to High-Performance Automated Theorem Proving (RB, ELL, WM, RAO), pp. 588–597.
CADE-1986-Chou #geometry #named #theorem proving: GEO-Prover — A Geometry Theorem Prover Developed at UT (SCC), pp. 679–680.
CADE-1986-GnaedigL #commutative #term rewriting #termination: Proving Termination of Associative Commutative Rewriting Systems by Rewriting (IG, PL), pp. 52–61.
CADE-1986-GreenbaumP #theorem proving: The Illinois Prover: A General Purpose Resolution Theorem Prover (SG, DAP), pp. 685–687.
CADE-1986-HsiangR #theorem proving: A New Method for Establishing Refutational Completeness in Theorem Proving (JH, MR), pp. 141–152.
CADE-1986-Huet: Mechanizing Constructive Proofs (GPH), p. 403.
CADE-1986-Huet86a #theorem proving: Theorem Proving Systems of the Formel Project (GPH), pp. 687–688.
CADE-1986-KapurNZ #induction #testing #using: Proof by Induction Using Test Sets (DK, PN, HZ), pp. 99–117.
CADE-1986-KutzlerS #algorithm #geometry #theorem proving: A Geometry Theorem Prover Based on Buchberger’s Algorithm (BK, SS), pp. 693–694.
CADE-1986-LoganantharajM #graph #parallel #theorem proving: Parallel Theorem Proving with Connection Graphs (RL, RAM), pp. 337–352.
CADE-1986-OppacherS #deduction #heuristic: Controlling Deduction with Proof Condensation and Heuristics (FO, ES), pp. 384–393.
CADE-1986-Stickel #compilation #implementation #prolog #theorem proving: A prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler (MES), pp. 573–587.
CADE-1986-ThistlewaiteMM #automation #theorem proving: The KRIPKE Automated Theorem Proving System (PBT, MAM, RKM), pp. 705–706.
CADE-1986-Wang #named #similarity: ECR: An Equality Conditional Resolution Proof Procedure (TCW), pp. 254–271.
LICS-1986-BachmairDH #equation #order: Orderings for Equational Proofs (LB, ND, JH), pp. 346–357.
LICS-1986-Brookes #concurrent #correctness #csp #semantics: A Semantically Based Proof System for Partial Correctness and Deadlock in CSP (SDB), pp. 58–65.
LICS-1986-ChouK #geometry #on the #theorem proving: On Mechanical Theorem Proving in Minkowskian Plane Geometry (SCC, HPK), pp. 187–192.
LICS-1986-Despeyroux #semantics: Proof of Translation in Natural Semantics (JD), pp. 193–205.
LICS-1986-JouannaudK #automation #equation #induction: Automatic Proofs by Induction in Equational Theories Without Constructors (JPJ, EK), pp. 358–366.
LICS-1986-Mason #equivalence #first-order #lisp #source code: Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via Transformation (IAM), pp. 105–117.
SLP-1986-Bledsoe86: Some Thoughts on Proof Discovery (WWB), pp. 2–10.
ICALP-1985-Hansel #theorem: A Simple Proof of the Skolem-Mahler-Lech Theorem (GH), pp. 244–249.
ICALP-1985-Stirling #composition #set: A Complete Compositional Model Proof System for a Subset of CCS (CS), pp. 475–486.
RTA-1985-ChoppyJ #named #petri net #term rewriting: PETRIREVE: Proving Petri Net Properties with Rewriting Systems (CC, CJ), pp. 271–286.
RTA-1985-DetlefsF #automation #set #termination: A Procedure for Automatically Proving the Termination of a Set of Rewrite Rules (DD, RF), pp. 255–270.
RTA-1985-Hsiang #term rewriting #theorem proving: Two Results in Term Rewriting Theorem Proving (JH), pp. 301–324.
POPL-1985-NguyenGO #network #process: A Model and Temporal Proof System for Networks of Processes (VN, DG, SSO), pp. 121–131.
AS-1985-Jones #design: The Role of Proof Obligations in Software Design (CBJ), pp. 27–41.
CAAP-1985-ChoppyGK #algebra #compilation #lisp #semantics: A Lisp Compiler for FP Language and Its Proof via Algebraic Semantics (CC, GG, SK), pp. 403–415.
CAAP-1985-KapurNS #order #term rewriting #termination: A Path Ordering for Proving Termination of Term Rewriting Systems (DK, PN, GS), pp. 173–187.
CAAP-1985-Karr #λ-calculus: “Delayability” in Proofs of Strong Normalizability in the Typed Lambda Calculus (MK), pp. 208–222.
CAAP-1985-Sterling #set: A Complete Modal Proof System for a Subset of SCCS (CS), pp. 253–266.
POPL-1984-RepsA #interactive: Interactive Proof Checking (TWR, BA), pp. 36–45.
ICSE-1984-Chyou #correctness: Structure Charts and Program Correctness Proofs (SCC), pp. 486–498.
CADE-1984-KapurK: A Natural Proof System Based on rewriting Techniques (DK, BK), pp. 53–64.
CADE-1984-Ketonen #named: EKL — A Mathematically Oriented Proof Checker (JK), pp. 65–79.
CADE-1984-Miller #deduction: Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs (DM), pp. 375–393.
CADE-1984-Mulmuley #recursion: The Mechanization of Existence Proofs of Recursive Predicates (KM), pp. 460–475.
CADE-1984-OhlbachW #automation #logic #problem #theorem proving: Solving a Problem in Relevance Logic with an Automated Theorem Prover (HJO, GW), pp. 496–508.
CADE-1984-Pfenning: Analytic and Non-analytic Proofs (FP), pp. 394–413.
CADE-1984-Plaisted #analysis #dependence #graph #theorem proving #using: Using Examples, Case Analysis, and Dependency Graphs in Theorem Proving (DAP), pp. 356–374.
CADE-1984-Stickel #case study #commutative #theorem proving: A Case Study of Theorem Proving by the Knuth-Bendix Method: Discovering That x³=x Implies Ring Commutativity (MES), pp. 248–258.
CADE-1984-Suppes #generative #interactive #theorem proving: The Next Generation of Interactive Theorem Provers (PS), pp. 303–315.
SLP-1984-AponteFR84 #editing #first-order: Editing First-Order Proofs: Programmed Rules vs Derived Rules (MVA, JAF, PR), pp. 92–98.
SLP-1984-Stickel84 #prolog #theorem proving: A Prolog Technology Theorem Prover (MES), pp. 211–217.
ICALP-1983-HsiangD #theorem proving: Rewrite Methods for Clausal and Non-Clausal Theorem Proving (JH, ND), pp. 331–346.
ICALP-1983-MannaP #precedence: Proving Precedence Properties: The Temporal Way (ZM, AP), pp. 491–512.
POPL-1983-MannaP #how: How to Cook a Temporal Proof System for Your Pet Language (ZM, AP), pp. 141–154.
POPL-1983-NagleJ #automation #embedded #realtime #verification: Practical Program Verification: Automatic Program Proving for Real-Time Embedded Software (JN, SJ), pp. 48–58.
ICALP-1982-Ben-Ari #algorithm #garbage collection #on the fly: On-the-Fly Garbage Collection: New Algorithms Inspired by Program Proofs (MBA), pp. 14–22.
STOC-1982-PachlKR #algorithm #bound #distributed: A Technique for Proving Lower Bounds for Distributed Maximum-Finding Algorithms (JKP, EK, DR), pp. 378–382.
CADE-1982-Caferra #matrix #reduction #validation: Proof by Matrix Reduction as Plan + Validation (RC), pp. 309–325.
ILPC-1982-BarbutiDL82 #logic programming #source code #towards: Toward an Inductionless Technique for Proving Properties of Logic Programs (RB, PD, GL), pp. 175–181.
VLDB-1981-BorgidaW #modelling #semantics: Data Models and Data Manipulation Languages: Complementary Semantics and Proof Theory (AB, HKTW), pp. 260–271.
ICALP-1981-Pettorossi #order #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.
ICALP-1981-Snir #bound: Proving Lower Bounds for Linar Decision Trees (MS), pp. 305–315.
ICSE-1981-BaerGGR #modelling #protocol #specification: The Two-Step Commitment Protocol: Modeling, Specification and Proof Methodology (JLB, GG, CG, GR), pp. 363–373.
ICSE-1981-RamamrithamK #process #specification: Specifying and Proving Properties of Sentinel Processes (KR, RMK), pp. 374–386.
DAC-1981-McFarland #automation #correctness #design #on the #optimisation: On proving the correctness of optimizing transformations in a digital design automation system (MCM), pp. 90–97.
SOSP-1981-BernsteinH #logic #realtime #source code: Proving Real-Time Properties of Programs with Temporal Logic (AJB, PKHJ), pp. 1–11.
ICALP-1980-Turchin #optimisation #theorem proving #using: The Use of Metasystem Transition in Theorem Proving and Program Optimization (VFT), pp. 645–657.
POPL-1980-Musser #data type #induction #on the: On Proving Inductive Properties of Abstract Data Types (DRM), pp. 154–162.
SDCG-1980-ThatcherWW #compilation: More on advice on structuring compilers and proving them correct (JWT, EGW, JBW), pp. 165–188.
CADE-1980-Andrews #deduction: Transforming Matings into Natural Deduction Proofs (PBA), pp. 281–292.
CADE-1980-BledsoeH: Variable Elimination and Chaining in a Resolution-based Prover for Inequalities (WWB, LMH), pp. 70–87.
CADE-1980-EricksonM #scalability #theorem proving: The AFFIRM Theorem Prover: Proof Forests and Management of Large Proofs (RWE, DRM), pp. 220–231.
CADE-1980-Gloess #correctness #empirical #parsing #theorem proving: An Experiment with the Boyer-Moore Theorem Prover: A Proof of the Correctness of a Simple Parser of Expressions (PYG), pp. 154–169.
CADE-1980-Goad: Proofs as Description of Computation (CG), pp. 39–52.
CADE-1980-Kott #recursion #source code: A System for Proving Equivalences of Recursive Programs (LK), pp. 63–69.
CADE-1980-Nederpelt #approach #theorem proving #λ-calculus: An Approach to Theorem Proving on the Basis of a Typed Lambda-Calculus (RN), pp. 182–194.
CADE-1980-Plaisted #abstraction #theorem proving: Abstraction Mappings in Mechanical Theorem Proving (DAP), pp. 264–280.
VLDB-1979-GardarinM #consistency #database #transaction: Proving Consistency of Database Transactions (GG, MAM), pp. 291–298.
ICALP-1979-DershowitzM #multi #order #termination: Proving termination with Multiset Orderings (ND, ZM), pp. 188–202.
ICALP-1979-DuncanY #algorithm #correctness: Studies in Abstract/Concrete Mappings in Proving Algorithm Correctness (AGD, LY), pp. 218–229.
ICALP-1979-ThatcherWW #compilation: More on Advice on Structuring Compilers and Proving Them Correct (JWT, EGW, JBW), pp. 596–615.
POPL-1979-GoodC #source code: Principles of Proving Programs Correct in Gypsy (DIG, RMC, JKW), pp. 42–52.
POPL-1978-German #automation #fault #runtime: Automating Proofs of the Absence of Common Runtime Errors (SMG), pp. 105–118.
POPL-1978-GordonMMNW #interactive #metalanguage: A Metalanguage for Interactive Proof in LCF (MJCG, RM, LM, MCN, CPW), pp. 119–130.
STOC-1978-Dowd #representation: Propositional Representation of Arithmetic Proofs (MD), pp. 246–252.
ICALP-1977-AptB #pascal #semantics: Semantics and Proof Theory of Pascal Procedures (KRA, JWdB), pp. 30–44.
POPL-1977-DeMilloLP #process #social #source code #theorem: Social Processes and Proofs of Theorems and Programs (RAD, RJL, AJP), pp. 206–214.
SOSP-1977-FeiertagLR #design #multi #security: Proving Multilevel Security of a System Design (RJF, KNL, LR), pp. 57–65.
STOC-1977-HarelPS #axiom #deduction #recursion #source code: A Complete Axiomatic System for Proving Deductions about Recursive Programs (DH, AP, JS), pp. 249–260.
STOC-1977-Hartmanis #complexity: Relations Between Diagonalization, Proof Systems, and Complexity Gaps (JH), pp. 223–227.
ICALP-1976-Brand #source code: Proving Programs Incorrect (DB), pp. 201–227.
ICALP-1976-Galil #integer #on the #programming #theorem proving: On Enumeration Procedures for Theorem Proving and for Integer Programming (ZG), pp. 355–381.
ICALP-1976-Greif #on the #source code: On Proofs of Programs for Synchronization (IG), pp. 494–507.
ICALP-1976-Schwarz #reasoning #source code #termination: Event Based Reasoning — A System for Proving Correct Termination of Programs (JS), pp. 131–146.
POPL-1976-Geller #correctness #testing: Test Data as an Aid in Proving Program Correctness (MMG), pp. 209–218.
ICSE-1976-Gries #correctness #source code: An Illustration of Current Ideas on the Derivation of Correctness Proofs and Correct Programs (DG), p. 200.
ICSE-1976-MannaW #correctness: Is “Sometime” Sometimes Better Than “Always”? Intermittent Assertions in Proving Program Correctness (ZM, RJW), pp. 32–39.
ICSE-1976-NeumannFLR #development #multi #security: Software Development and Proofs of Multi-Level Security (PGN, RJF, KNL, LR), pp. 421–428.
SOSP-J-1975-Howard76 #monitoring: Proving Monitors (JHH), pp. 273–279.
POPL-1975-Lipton #named #process #reduction: Reduction: A New Method of Proving Properties of Systems of Processes (RJL), pp. 78–86.
STOC-1975-Cook #calculus: Feasibly Constructive Proofs and the Propositional Calculus (SAC), pp. 83–97.
STOC-1975-OppenC #data type #source code: Proving Assertions about Programs that Manipulate Data Structures (DCO, SAC), pp. 107–116.
STOC-1975-RivestV: A Generalization and Proof of the Aanderaa-Rosenberg Conjecture (RLR, JV), pp. 6–11.
STOC-1974-CookR #calculus #on the: On the Lengths of Proofs in the Propositional Calculus (SAC, RAR), pp. 135–148.
POPL-1973-Morris73a #compilation: Advice on Structuring Compilers and Proving Them Correct (FLM), pp. 144–152.
SIGFIDET-1972-HawryszkiewyczD #approach #correctness #database: An Approach to Proving the Correctness of Data Base Operations (IH, JBD), pp. 323–348.
ICALP-1972-HitchcockP #induction #termination: Induction Rules and Termination Proofs (PH, DMRP), pp. 225–251.
STOC-1970-KingF #integer #theorem proving: An Interpretation Oriented Theorem Prover over Integers (JCK, RWF), pp. 169–179.
STOC-1970-Reiter #theorem proving: The Predicate Elimination Strategy in Theorem Proving (RR), pp. 180–183.
STOC-1970-Rounds #theorem: Tree-Oriented Proofs of Some Theorems on Context-Free and Indexed Languages (WCR), pp. 109–116.