BibSLEIGH — Edmund_M

Travelled to:

1 × Austria
1 × Croatia
1 × Finland
1 × Greece
1 × Hungary
1 × Israel
1 × Poland
1 × Portugal
1 × Russia
1 × Spain
1 × Turkey
2 × France
2 × Germany
3 × Canada
3 × Denmark
3 × The Netherlands
38 × USA
4 × Italy
9 × United Kingdom

Collaborated with:

∅ O.Grumberg X.Zhao D.Kröning S.Jha H.Veith S.Chaki H.Jain S.Gao K.L.McMillan D.E.Long N.Sharygina N.Sinha M.Talupur E.A.Emerson A.P.Sistla A.Platzer S.M.German A.Biere A.Komuravelli S.V.A.Campos A.Cimatti M.Minea W.R.Marrero J.R.Burch Y.Lu Y.Zhu C.S.Pasareanu J.Avigad J.Y.Halpern M.Fujita J.Ouaknine S.Kong K.Yorav Y.Chen A.Farzan Y.Tsay B.Wang W.Klieber O.Strichman D.Wang A.Gupta S.Bose S.Michaylov Y.Feng A.Gurfinkel S.Sapra V.Hartonas-Garmhausen D.L.Dill F.Giunchiglia M.Roveri T.Touili C.Bartzis P.Chauhan F.Lerda M.Khaira K.Hamaguchi T.Filkorn P.A.Bernstein B.T.Blaustein M.C.Browne W.Chen M.Janota J.Marques-Silva S.Magill J.Berdine B.Cook P.Thati J.H.Kukula P.F.Williams J.Jain R.Raimi T.Yoneda A.Shibayama B.Schlingloff P.E.Allen T.S.Anantharaman M.J.Foster B.Mishra N.Kidd T.W.Reps A.Groce A.Campailla C.Baier M.Z.Kwiatkowska M.Ryan A.Browne J.Yang L.J.Hwang M.Tsai A.Fehnker Z.Han B.H.Krogh O.Stursberg M.Theobald P.Cerný T.A.Henzinger A.Radhakrishna L.Ryzhyk R.Samanta T.Tarrach E.Giunchiglia M.Pistore R.Sebastiani A.Tacchella

Talks about:

check (28) model (26) use (16) system (15) symbol (15) verif (15) abstract (14) base (10) effici (9) state (9)

Person: Edmund M. Clarke

DBLP: Clarke:Edmund_M=

Facilitated 1 volumes:

Contributed to:

2015

2013

2012

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

1995

1994

1993

1992

1991

1990

1989

1988

1986

1985

1983

1982

1980

1979

1977

1987

Wrote 90 papers:

CAV-2015-CernyCHRRST #scheduling #synthesis #using: From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis (PC, EMC, TAH, AR, LR, RS, TT), pp. 180–197.
TACAS-2015-KongGCC #analysis #hybrid #named: dReach: δ-Reachability Analysis for Hybrid Systems (SK, SG, WC, EMC), pp. 200–205.
CADE-2013-GaoKC #named #smt: dReal: An SMT Solver for Nonlinear Theories over the Reals (SG, SK, EMC), pp. 208–214.
CAV-2013-KomuravelliGCC #abstraction #automation #bound #model checking #smt: Automatic Abstraction in SMT-Based Unbounded Software Model Checking (AK, AG, SC, EMC), pp. 846–862.
ICTSS-2013-SapraMCGC #execution #fault #python #source code #symbolic computation #using: Finding Errors in Python Programs Using Dynamic Symbolic Execution (SS, MM, SC, AG, EMC), pp. 283–289.
SAT-2013-Clarke #why: Turing’s Computable Real Numbers and Why They Are Still Important Today (EMC), p. 18.
CAV-2012-KomuravelliPC #abstraction #probability #refinement: Assume-Guarantee Abstraction Refinement for Probabilistic Systems (AK, CSP, EMC), pp. 310–326.
IJCAR-2012-GaoAC #satisfiability: δ-Complete Decision Procedures for Satisfiability over the Reals (SG, JA, EMC), pp. 286–300.
LICS-2012-GaoAC: Delta-Decidability over the Reals (SG, JA, EMC), pp. 305–314.
LICS-2012-KomuravelliPC #learning #probability: Learning Probabilistic Systems from Tree Samples (AK, CSP, EMC), pp. 441–450.
SAT-2012-JanotaKMC #refinement: Solving QBF with Counterexample Guided Refinement (MJ, WK, JMS, EMC), pp. 114–128.
CAV-2010-ChenCFTTW #automation #learning #reasoning: Automated Assume-Guarantee Reasoning through Implicit Learning (YFC, EMC, AF, MHT, YKT, BYW), pp. 511–526.
SAT-2010-KlieberSGC #learning: A Non-prenex, Non-clausal QBF Solver with Game-State Learning (WK, SS, SG, EMC), pp. 128–142.
DAC-2009-JainC #graph #performance #satisfiability #using: Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts (HJ, EMC), pp. 563–568.
FM-2009-PlatzerC #case study #verification: Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study (AP, EMC), pp. 547–562.
LICS-2009-Clarke #explosion #problem: My 27-year Quest to Overcome the State Explosion Problem (EMC), p. 3.
TACAS-2009-ChenFCTW #automaton #composition #learning #verification: Learning Minimal Separating DFA’s for Compositional Verification (YFC, AF, EMC, YKT, BYW), pp. 31–45.
CAV-2008-JainCG #composition #equation #linear #performance: Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular Equations (HJ, EMC, OG), pp. 254–267.
CAV-2008-PlatzerC #difference #hybrid #invariant: Computing Differential Invariants of Hybrid Systems as Fixedpoints (AP, EMC), pp. 176–189.
TACAS-2008-ClarkeTV #abstraction #concurrent #framework #model checking #proving: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems (EMC, MT, HV), pp. 33–47.
TACAS-2008-FarzanCCTW #automation #composition #regular expression #verification: Extending Automated Compositional Verification to the Full Class of ω-Regular Languages (AF, YFC, EMC, YKT, BYW), pp. 2–17.
CAV-2007-SinhaC #composition #lazy evaluation #learning #satisfiability #using #verification: SAT-Based Compositional Verification Using Lazy Learning (NS, EMC), pp. 39–54.
SAS-2007-MagillBCC #analysis: Arithmetic Strengthening for Shape Analysis (SM, JB, EMC, BC), pp. 419–436.
TACAS-2007-JainKSC #abstraction #named #refinement: VCEGAR: Verilog CounterExample Guided Abstraction Refinement (HJ, DK, NS, EMC), pp. 583–586.
SAT-2006-JainBC #satisfiability #using: Satisfiability Checking of Non-clausal Formulas Using General Matings (HJ, CB, EMC), pp. 75–89.
TACAS-2006-ChakiCKRT #c #concurrent #message passing #recursion #source code #verification: Verifying Concurrent Message-Passing C Programs with Recursive Calls (SC, EMC, NK, TWR, TT), pp. 334–349.
VMCAI-2006-ClarkeTV #abstraction #verification: Environment Abstraction for Parameterized Verification (EMC, MT, HV), pp. 126–141.
CAV-2005-ChakiCST #automation #consistency #reasoning #simulation: Automated Assume-Guarantee Reasoning for Simulation Conformance (SC, EMC, NS, PT), pp. 534–547.
DAC-2005-JainKSC #abstraction #refinement #verification #word: Word level predicate abstraction and refinement for verifying RTL verilog (HJ, DK, NS, EMC), pp. 445–450.
FM-2005-SharyginaCCS #analysis #component: Dynamic Component Substitutability Analysis (NS, SC, EMC, NS), pp. 512–528.
IFM-2005-ChakiCGOSTV #specification #verification: State/Event Software Verification for Branching-Time Specifications (SC, EMC, OG, JO, NS, TT, HV), pp. 53–69.
TACAS-2005-ClarkeKSY #abstraction #named #satisfiability: SATABS: SAT-Based Predicate Abstraction for ANSI-C (EMC, DK, NS, KY), pp. 570–574.
DAC-2004-ChauhanCK #algorithm #satisfiability #simulation: A SAT-based algorithm for reparameterization in symbolic simulation (PC, EMC, DK), pp. 524–529.
IFM-2004-ChakiCOSS #model checking: State/Event-Based Software Model Checking (SC, EMC, JO, NS, NS), pp. 128–147.
TACAS-2004-ClarkeKL #source code: A Tool for Checking ANSI-C Programs (EMC, DK, FL), pp. 168–176.
VMCAI-2004-ClarkeKOS #bound #complexity #model checking: Completeness and Complexity of Bounded Model Checking (EMC, DK, JO, OS), pp. 85–96.
CADE-2003-Clarke #abstraction #model checking #refinement #satisfiability: SAT-Based Counterexample Guided Abstraction Refinement in Model Checking (EMC), p. 1.
CAV-2003-ClarkeGTW #abstraction #how #performance: Making Predicate Abstraction Efficient: How to Eliminate Redundant Predicates (EMC, OG, MT, DW), pp. 126–140.
DAC-2003-ClarkeKY #behaviour #bound #c #consistency #model checking #source code #using: Behavioral consistency of C and verilog programs using bounded model checking (EMC, DK, KY), pp. 368–371.
ICSE-2003-ChakiCGJV #c #component #composition #verification: Modular Verification of Software Components in C (SC, EMC, AG, SJ, HV), pp. 385–395.
SAT-2003-ClarkeTVW #abstraction #hardware #satisfiability #verification: SAT Based Predicate Abstraction for Hardware Verification (EMC, MT, HV, DW), pp. 78–92.
TACAS-2003-ClarkeFHKST #abstraction #hybrid #refinement #verification: Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement (EMC, AF, ZH, BHK, OS, MT), pp. 192–207.
CAV-2002-CimattiCGGPRST #model checking: NuSMV 2: An OpenSource Tool for Symbolic Model Checking (AC, EMC, EG, FG, MP, MR, RS, AT), pp. 359–364.
CAV-2002-ClarkeGKS #abstraction #machine learning #satisfiability #using: SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques (EMC, AG, JHK, OS), pp. 265–279.
LICS-2002-ClarkeJLV #model checking: Tree-Like Counterexamples in Model Checking (EMC, SJ, YL, HV), pp. 19–29.
ICSE-2001-CampaillaCCJV #performance #using: Efficient Filtering in Publish-Subscribe Systems Using Binary Decision (AC, SC, EMC, SJ, HV), pp. 443–452.
CAV-2000-ClarkeGJLV #abstraction #refinement: Counterexample-Guided Abstraction Refinement (EMC, OG, SJ, YL, HV), pp. 154–169.
CAV-2000-WilliamsBCG #diagrams #model checking #performance #satisfiability: Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking (PFW, AB, EMC, AG), pp. 124–138.
DAC-2000-LuJCF #performance #using: Efficient variable ordering using aBDD based sampling (YL, JJ, EMC, MF), pp. 687–692.
TACAS-2000-ClarkeJM #partial order #protocol #reduction #security #verification: Partial Order Reductions for Security Protocol Verification (EMC, SJ, WRM), pp. 503–518.
CAV-1999-BiereCRZ #model checking #safety #using: Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs (AB, EMC, RR, YZ), pp. 60–71.
CAV-1999-CimattiCGR #named #verification: NUSMV: A New Symbolic Model Verifier (AC, EMC, FG, MR), pp. 495–499.
DAC-1999-BiereCCFZ #model checking #satisfiability #using: Symbolic Model Checking Using SAT Procedures instead of BDDs (AB, AC, EMC, MF, YZ), pp. 317–320.
TACAS-1999-BiereCCZ #model checking: Symbolic Model Checking without BDDs (AB, AC, EMC, YZ), pp. 193–207.
CAV-1998-ClarkeEJS #model checking #reduction #symmetry: Symmetry Reductions inModel Checking (EMC, EAE, SJ, APS), pp. 147–158.
CAV-1997-CamposCM #approach #realtime #verification: The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems (SVAC, EMC, MM), pp. 452–455.
ICALP-1997-BaierCHKR #model checking #probability #process: Symbolic Model Checking for Probabilistic Processes (CB, EMC, VHG, MZK, MR), pp. 430–440.
ILPS-1997-Clarke #logic #model checking: Temporal Logic Model Checking (EMC), p. 3.
CAV-1996-ClarkeGZ #algorithm #proving #theorem proving #using #verification: Verifying the SRT Division Algorithm Using Theorem Proving Techniques (EMC, SMG, XZ), pp. 111–122.
CAV-1996-ClarkeMCH #model checking: Symbolic Model Checking (EMC, KLM, SVAC, VHG), pp. 419–427.
DAC-1996-ClarkeKZ #fault #model checking #word: Word Level Model Checking — Avoiding the Pentium FDIV Error (EMC, MK, XZ), pp. 645–648.
DAC-1995-ClarkeGMZ #generative #model checking #performance: Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking (EMC, OG, KLM, XZ), pp. 427–432.
LCT-RTS-1995-CamposCMM #analysis #finite #named #realtime: Verus: A Tool for Quantitative Analysis of Finite-State Real-Time Systems (SVAC, EMC, WRM, MM), pp. 70–78.
CADE-1994-ClarkeZ #problem #proving #symbolic computation #theorem proving: Combining Symbolic Computation and Theorem Proving: Some Problems of Ramanujan (EMC, XZ), pp. 758–763.
CAV-1994-ClarkeGH #ltl #model checking: Another Look at LTL Model Checking (EMC, OG, KH), pp. 415–427.
CAV-1994-LongBCJM #algorithm #evaluation #fixpoint: An Improved Algorithm for the Evaluation of Fixpoint Expressions (DEL, AB, EMC, SJ, WRM), pp. 338–350.
LICS-1994-Clarke #automation #concurrent #finite #verification: Automatic Verification of Finite-State Concurrent Systems (EMC), p. 126.
CAV-1993-ClarkeFJ #logic #model checking #symmetry: Exploiting Symmetry In Temporal Logic Model Checking (EMC, TF, SJ), pp. 450–462.
CAV-1993-YonedaSSC #parallel #performance #realtime #verification: Efficient Verification of Parallel Real-Time Systems (TY, AS, BHS, EMC), pp. 321–346.
DAC-1993-ClarkeMZFY #scalability: Spectral Transforms for Large Boolean Functions with Applications to Technology Mapping (EMC, KLM, XZ, MF, JY), pp. 54–60.
CADE-1992-ClarkeZ #named #proving #theorem proving: Analytica — A Theorem Prover in Mathematica (EMC, XZ), pp. 761–765.
POPL-1992-ClarkeGL #abstraction #model checking: Model Checking and Abstraction (EMC, OG, DEL), pp. 342–354.
DAC-1991-BurchCL #model checking #representation: Representing Circuits More Efficiently in Symbolic Model Checking (JRB, EMC, DEL), pp. 403–407.
CAV-1990-Clarke #explosion #logic #model checking #problem: Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem (EMC), p. 1.
DAC-1990-BurchCMD #model checking #using #verification: Sequential Circuit Verification Using Symbolic Model Checking (JRB, EMC, KLM, DLD), pp. 46–51.
LICS-1990-BurchCMDH #model checking: Symbolic Model Checking: 10^20 States and Beyond (JRB, EMC, KLM, DLD, LJH), pp. 428–439.
LICS-1989-BoseCLM #horn clause #named #parallel #proving #theorem proving: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (SB, EMC, DEL, SM), pp. 80–89.
LICS-1989-ClarkeLM #composition #model checking: Compositional Model Checking (EMC, DEL, KLM), pp. 353–362.
CADE-1988-AllenBCM #horn clause #named #parallel #proving #theorem proving: PARTHENON: A Parallel Theorem Prover for Non-Horn Clauses (PEA, SB, EMC, SM), pp. 764–765.
DAC-1986-ClarkeF #geometry #layout #named #recursion: Escher — a geometrical layout system for recursively defined circuits (EMC, YF), pp. 650–653.
LICS-1986-GermanCH #axiom: True Relative Completeness of an Axiom System for the Language L4 (Abridged) (SMG, EMC, JYH), pp. 11–25.
POPL-1985-AnantharamanCFM #compilation: Compiling Path Expressions into VLSI Circuits (TSA, EMC, MJF, BM), pp. 191–204.
POPL-1983-ClarkeES #approach #automation #concurrent #finite #logic #specification #using #verification: Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach (EMC, EAE, APS), pp. 117–126.
POPL-1982-ClarkeGH #axiom #effectiveness #hoare #logic #on the: On Effective Axiomatizations of Hoare Logics (EMC, SMG, JYH), pp. 309–321.
STOC-1982-SistlaC #complexity #linear #logic: The Complexity of Propositional Linear Temporal Logics (APS, EMC), pp. 159–168.
ICALP-1980-EmersonC #correctness #fixpoint #parallel #source code #using: Characterizing Correctness Properties of Parallel Programs Using Fixpoints (EAE, EMC), pp. 169–181.
VLDB-1980-BernsteinBC #maintenance #performance #semantics #using: Fast Maintenance of Semantic Integrity Assertions Using Redundant Aggregate Data (PAB, BTB, EMC), pp. 126–136.
POPL-1979-Clarke #concurrent #invariant #source code #synthesis: Synthesis of Resource Invariants for Concurrent Programs (EMC), pp. 211–221.
POPL-1977-Clarke #axiom #hoare #programming language: Programming Language Constructs for Which it is Impossible to Obtain “Good” Hoare-Like Axiom Systems (EMC), pp. 10–20.
CAAP-1987-BrowneCG #logic: Characterizing Kripke Structures in Temporal Logic (MCB, EMC, OG), pp. 256–270.