BibSLEIGH — David_L

Travelled to:

1 × Belgium
1 × Germany
1 × Greece
1 × Israel
1 × Italy
1 × Poland
1 × Spain
22 × USA
3 × Canada
3 × Denmark

Collaborated with:

∅ A.J.Hu C.W.Barrett A.Stump H.Wong-Toi U.Stern R.Alur S.Berezin C.N.Ip J.R.Burch C.Courcoubetis V.Ganesh S.Das S.Park C.H.Yang J.R.Levitt J.U.Skakkebæk S.G.Govindaraju K.Shimizu C.Wilson P.Loewenstein D.Y.W.Park E.M.Clarke K.L.McMillan J.Chang H.Abu-Haimed J.P.Bergmann R.B.Jones G.York P.Siegel G.D.Micheli G.Katz K.Julian M.J.Kochenderfer M.Horowitz M.Chatzaki P.Tzounakis A.J.Drexler M.D.Linderman M.Ho T.H.Y.Meng G.P.Nolan D.Sahoo J.Jain S.K.Iyer E.A.Emerson M.Musuvathi A.Chou D.R.Engler L.J.Hwang N.James S.Rawat G.Berry L.Fix H.Foster R.K.Ranjan G.Stålmarck C.Widdoes D.A.Huang D.Ibeling C.Lazarus R.Lim P.Shah S.Thakoor H.W.0001 A.Zeljic

Talks about:

verif (17) check (11) use (11) model (9) system (6) real (6) procedur (5) formal (5) simul (5) decis (5)

Person: David L. Dill

DBLP: Dill:David_L=

Facilitated 1 volumes:

Contributed to:

2012

2011

2010

2007

2006

2005

2004

2003

2002

2001

2000

1999

1998

1997

1996

1995

1994

1993

1992

1991

1990

2017

2019

Wrote 53 papers:

CAV-2012-Dill #biology #model checking: Model Checking Cell Biology (DLD), p. 2.
VMCAI-2011-Dill: Are Cells Asynchronous Circuits? — (DLD), p. 1.
CGO-2010-LindermanHDMN #analysis #automation #optimisation #precise #towards: Towards program optimization through automated analysis of numerical precision (MDL, MH, DLD, THYM, GPN), pp. 230–237.
CAV-2007-GaneshD #array: A Decision Procedure for Bit-Vectors and Arrays (VG, DLD), pp. 519–531.
CAV-2006-Dill: I Think I Voted: E-Voting vs. Democracy (DLD), p. 2.
DAC-2005-SahooJIDE #concurrent #multi #reachability #thread: Multi-threaded reachability (DS, JJ, SKI, DLD, EAE), pp. 467–470.
CAV-2004-ChangBD #design #interface #refinement #using #verification: Using Interface Refinement to Integrate Formal Verification into the Design Cycle (JC, SB, DLD), pp. 122–134.
CAV-2003-Abu-HaimedBD #consistency #invariant #testing: Strengthening Invariants by Symbolic Consistency Testing (HAH, SB, DLD), pp. 407–419.
TACAS-2003-BerezinGD #linear #online: An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic (SB, VG, DLD), pp. 521–536.
CADE-2002-StumpD #framework #logic #performance #proving: Faster Proof Checking in the Edinburgh Logical Framework (AS, DLD), pp. 392–407.
CAV-2002-BarrettDS #first-order #incremental #satisfiability: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT (CWB, DLD, AS), pp. 236–249.
CAV-2002-StumpBD #named: CVC: A Cooperating Validity Checker (AS, CWB, DLD), pp. 500–504.
DAC-2002-DillJRBFFRSW #verification: Formal verification methods: getting around the brick wall (DLD, NJ, SR, GB, LF, HF, RKR, GS, CW), pp. 576–577.
DAC-2002-ShimizuD #generative #metric #simulation #specification: Deriving a simulation input generator and a coverage metric from a formal specification (KS, DLD), pp. 801–806.
OSDI-2002-MusuvathiPCED #approach #model checking #named: CMC: A Pragmatic Approach to Model Checking Real Code (MM, DYWP, AC, DRE, DLD), pp. 75–88.
LICS-2001-DasD #approximate: Successive Approximation of Abstract Transition Relations (SD, DLD), pp. 51–58.
LICS-2001-StumpBDL #array: A Decision Procedure for an Extensional Theory of Arrays (AS, CWB, DLD, JRL), pp. 29–37.
ASE-2000-ParkSSD #java #model checking: Java Model Checking (DYWP, US, JUS, DLD), pp. 253–256.
CADE-2000-BarrettDS #framework: A Framework for Cooperating Decision Procedures (CWB, DLD, AS), pp. 79–98.
DAC-2000-WilsonD #reliability #simulation #using #verification: Reliable verification using symbolic simulation with scalar values (CW, DLD), pp. 124–129.
ISSTA-2000-Dill #java #model checking #source code: Model checking Java programs (DLD), p. 179.
CAV-1999-DasDP #abstraction #experience: Experience with Predicate Abstraction (SD, DLD, SP), pp. 160–171.
CAV-1999-Dill #hardware #verification: Alternative Approaches to Hardware Verification (DLD), p. 1.
DAC-1999-GovindarajuDB #approximate #reachability #using: Improved Approximate Reachability Using Auxiliary State Variables (SGG, DLD, JPB), pp. 312–316.
CAV-1998-SkakkebaekJD #execution #incremental #using #verification: Formal Verification of Out-of-Order Execution Using Incremental Flushing (JUS, RBJ, DLD), pp. 98–109.
CAV-1998-SternD #in memory #memory management #using #verification: Using Magnatic Disk Instead of Main Memory in the Murphi Verifier (US, DLD), pp. 172–183.
DAC-1998-BarrettDL: A Decision Procedure for Bit-Vector Arithmetic (CWB, DLD, JRL), pp. 522–527.
DAC-1998-Dill #question #simulation #verification #what: What’s Between Simulation and Formal Verification? (DLD), pp. 328–329.
DAC-1998-GovindarajuDHH #approximate #reachability #using: Approximate Reachability with BDDs Using Overlapping Projections (SGG, DLD, AJH, MH), pp. 451–456.
DAC-1998-YangD #validation: Validation with Guided Search of the State Space (CHY, DLD), pp. 599–604.
CAV-1997-SternD #verification: Parallelizing the Murphi Verifier (US, DLD), pp. 256–278.
CAV-1996-Dill #verification: The Murphi Verification System (DLD), pp. 390–393.
CAV-1996-IpD #component #verification: Verifying Systems with Replicated Components in Murphi (CNI, DLD), pp. 147–158.
CAV-1996-ParkD #distributed #protocol #transaction #verification: Protocol Verification by Aggregation of Distributed Transactions (SP, DLD), pp. 300–310.
DAC-1996-IpD #reduction #using: State Reduction Using Reversible Rules (CNI, DLD), pp. 564–567.
CAV-1995-DillW #approximate #realtime #verification: Verification of Real-Time Systems by Successive Over and Under Approximation (DLD, HWT), pp. 409–422.
CAV-1994-BurchD #automation #pipes and filters #verification: Automatic verification of Pipelined Microprocessor Control (JRB, DLD), pp. 68–80.
DAC-1994-HuYD #performance #verification: New Techniques for Efficient Verification with Implicitly Conjoined BDDs (AJH, GY, DLD), pp. 276–282.
CAV-1993-HuD #invariant #performance #using #verification: Efficient Verification with BDDs using Implicitly Conjoined Invariants (AJH, DLD), pp. 3–14.
DAC-1993-HuD #dependence #functional: Reducing BDD Size by Exploiting Functional Dependencies (AJH, DLD), pp. 266–271.
DAC-1993-SiegelMD #automation #design: Automatic Technology Mapping for Generalized Fundamental-Mode Asynchronous Designs (PS, GDM, DLD), pp. 61–67.
CAV-1992-CourcoubetisDCT #realtime #verification: Verification with Real-Time COSPAN (CC, DLD, MC, PT), pp. 274–287.
CAV-1992-HuDDY #specification #verification: Higher-Level Specification and Verification with BDDs (AJH, DLD, AJD, CHY), pp. 82–95.
CAV-1991-DillHW #simulation #using: Checking for Language Inclusion Using Simulation Preorders (DLD, AJH, HWT), pp. 255–265.
ICALP-1991-AlurCD #model checking #probability #realtime: Model-Checking for Probabilistic Real-Time Systems (RA, CC, DLD), pp. 115–126.
CAV-1990-LoewensteinD #higher-order #logic #multi #protocol #simulation #using #verification: Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic (PL, DLD), pp. 302–311.
CAV-1990-Wong-ToiD #process #specification: Synthesizing Processes and Schedulers from Temporal Specifications (HWT, DLD), pp. 272–281.
DAC-1990-BurchCMD #model checking #using #verification: Sequential Circuit Verification Using Symbolic Model Checking (JRB, EMC, KLM, DLD), pp. 46–51.
ICALP-1990-AlurD #automaton #modelling #realtime: Automata For Modeling Real-Time Systems (RA, DLD), pp. 322–335.
LICS-1990-AlurCD #model checking #realtime: Model-Checking for Real-Time Systems (RA, CC, DLD), pp. 414–425.
LICS-1990-BurchCMDH #model checking: Symbolic Model Checking: 10^20 States and Beyond (JRB, EMC, KLM, DLD, LJH), pp. 428–439.
CAV-2017-KatzBDJK #named #network #performance #smt #verification: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (GK, CWB, DLD, KJ, MJK), pp. 97–117.
CAV-2019-KatzHIJLLSTWZDK #analysis #framework #network #verification: The Marabou Framework for Verification and Analysis of Deep Neural Networks (GK, DAH, DI, KJ, CL, RL, PS, ST, HW0, AZ, DLD, MJK, CWB), pp. 443–452.