BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
proving
Google proving

Tag #proving

1503 papers:

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

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