32 papers:
SAS-2015-Brain0KS #invariant #safety #verification- Safety Verification and Refutation by k-Invariants and k-Induction (MB, SJ, DK, PS), pp. 145–161.
ICSE-v1-2015-DeweyNH #automation #data type #generative- Automated Data Structure Generation: Refuting Common Wisdom (KD, LN, BH), pp. 32–43.
ICALP-v1-2014-Tzameret #algorithm #problem #random #satisfiability- Sparser Random 3-SAT Refutation Algorithms and the Interpolation Problem — (Extended Abstract) (IT), pp. 1015–1026.
IFM-2014-ErikssonPB #invariant #programming #proving- Proofs and Refutations in Invariant-Based Programming (JE, MP, RJB), pp. 189–204.
SAT-2014-FinkbeinerT #performance- Fast DQBF Refutation (BF, LT), pp. 243–251.
VMCAI-2014-Chang #reachability- Refuting Heap Reachability (BYEC), pp. 137–141.
PLDI-2013-BlackshearCS #named #precise #reachability- Thresher: precise refutations for heap reachability (SB, BYEC, MS), pp. 275–286.
CADE-2013-HeuleHW #verification- Verifying Refutations with Extended Resolution (MH, WAHJ, NW), pp. 345–359.
KR-2012-BordeauxJSM #on the #quantifier- On Unit-Refutation Complete Formulae with Existentially Quantified Variables (LB, MJ, JPMS, PM).
LICS-2012-MullerT #random- Short Propositional Refutations for Dense Random 3CNF Formulas (SM, IT), pp. 501–510.
FM-2008-McIverMG #probability #proving #refinement- Proofs and Refutations for Probabilistic Refinement (AKM, CCM, CG), pp. 100–115.
- LICS-2008-DelandeM #approach #proving
- A Neutral Approach to Proof and Refutation in MALL (OD, DM), pp. 498–508.
- SAT-2007-Buresh-OppenheimM #polynomial
- Minimum 2CNF Resolution Refutations in Polynomial Time (JBO, DGM), pp. 300–313.
CAV-2006-GurfinkelWC #model checking #named #verification- Yasm: A Software Model-Checker for Verification and Refutation (AG, OW, MC), pp. 170–174.
DATE-2005-ShenQL #algorithm #analysis #performance- A Faster Counterexample Minimization Algorithm Based on Refutation Analysis (SS, YQ, SL), pp. 672–677.
- ICALP-2004-FeigeO #random #scalability
- Easily Refutable Subformulas of Large Random 3CNF Formulas (UF, EO), pp. 519–530.
IJCAR-2004-SteelBM #induction #protocol- Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures (GS, AB, MM), pp. 137–151.
- CAV-2003-MouraRS #bound #induction #model checking #verification
- Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A) (LMdM, HR, MS), pp. 14–26.
- ICALP-2002-ImpagliazzoS #axiom #bound #simulation
- Bounded-Depth Frege Systems with Counting Axioms Polynomially Simulate Nullstellensatz Refutations (RI, NS), pp. 208–219.
CSL-2002-Beckmann #proving #strict- Resolution Refutations and Propositional Proofs with Height-Restrictions (AB), pp. 599–612.
- IJCAR-2001-Szeider
- NP-Completeness of Refutability by Literal-Once Resolution (SS), pp. 168–181.
- CSL-1998-Buning #bound
- An Upper Bound for Minimal Resolution Refutations (HKB), pp. 171–178.
RTA-1995-Nieuwenhuis #constraints #on the #proving- On Narrowing, Refutation Proofs and Constraints (RN), pp. 56–70.
- FME-1994-WangM
- RTL and Refutation by Positive Cycles (FW, AKM), pp. 659–680.
ICLP-1994-Mircheva #logic programming #source code- Logic Programs with Refutation Rules (MM), p. 734.
- LICS-1994-HofmannS #proving
- The Groupoid Model Refutes Uniqueness of Identity Proofs (MH, TS), pp. 208–212.
- ICLP-1991-KoN #revisited
- Substitution and Refutation Revisited (HPK, MEN), pp. 679–692.
- RTA-1991-Deruyver #equation #first-order #logic #named #proving #theorem proving
- EMMY: A Refutational Theorem Prover for First-Order Logic with Equation (AD), pp. 439–441.
- LICS-1989-Fitting
- Negation As Refutation (MF), pp. 63–70.
- CADE-1986-EisingerO
- The Markgraf Karl Refutation Procedure (MKRP) (NE, HJO), pp. 681–682.
- CADE-1986-HsiangR #proving #theorem proving
- A New Method for Establishing Refutational Completeness in Theorem Proving (JH, MR), pp. 141–152.
- CADE-1986-Schneider #deduction
- An Improvement of Deduction Plans: Refutation Plans (HAS), pp. 377–383.
