Proceedings of the 12th International Conference on Computer Aided Verification
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

E. Allen Emerson, A. Prasad Sistla
Proceedings of the 12th International Conference on Computer Aided Verification
CAV, 2000.

TEST
DBLP
Scholar
Full names Links ISxN
@proceedings{CAV-2000,
	address       = "Chicago, Illinois, USA",
	editor        = "E. Allen Emerson and A. Prasad Sistla",
	isbn          = "3-540-67770-4",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 12th International Conference on Computer Aided Verification}",
	volume        = 1855,
	year          = 2000,
}

Contents (48 items)

CAV-2000-Pnueli #abstraction #composition #deduction #explosion #symmetry
Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion (AP), p. 1.
CAV-2000-Meadows #analysis #encryption #formal method #protocol
Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis (CM), p. 2.
CAV-2000-Marques-SilvaS #algorithm #automation #design #satisfiability #tutorial
Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation (JPMS, KAS), p. 3.
CAV-2000-AbdullaJ #infinity #tutorial #verification
Invited Tutorial: Verification of Infinite-State and Parameterized Systems (PAA, BJ), p. 4.
CAV-2000-BaumgartnerTASA #abstraction #algorithm #design #verification
An Abstraction Algorithm for the Verification of Generalized C-Slow Designs (JB, AT, AA, VS, FA), pp. 5–19.
CAV-2000-HeymanGGS #analysis #parallel #reachability #scalability
Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits (TH, DG, OG, AS), pp. 20–35.
CAV-2000-KupfermanV #approach #infinity #reasoning
An Automata-Theoretic Approach to Reasoning about Infinite-State Systems (OK, MYV), pp. 36–52.
CAV-2000-Delzanno #automation #protocol #verification
Automatic Verification of Parameterized Cache Coherence Protocols (GD), pp. 53–68.
CAV-2000-DangIBKS #analysis #automaton #reachability
Binary Reachability Analysis of Discrete Pushdown Timed Automata (ZD, OHI, TB, RAK, JS), pp. 69–84.
CAV-2000-BryantV #constraints #satisfiability #transitive
Boolean Satisfiability with Transitivity Constraints (REB, MNV), pp. 85–98.
CAV-2000-AyariB #bound #higher-order #logic #monad
Bounded Model Construction for Monadic Second-Order Logics (AA, DAB), pp. 99–112.
CAV-2000-KukulaS
Building Circuits from Relations (JHK, TRS), pp. 113–123.
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.
CAV-2000-NamjoshiT #composition #on the #reasoning
On the Competeness of Compositional Reasoning (KSN, RJT), pp. 139–153.
CAV-2000-ClarkeGJLV #abstraction #refinement
Counterexample-Guided Abstraction Refinement (EMC, OG, SJ, YL, HV), pp. 154–169.
CAV-2000-AyariBK #automaton #induction
Decision Procedures for Inductive Boolean Functions Based on Alternating Automata (AA, DAB, FK), pp. 170–185.
CAV-2000-AlfaroHM #detection #fault
Detecting Errors Before Reaching Them (LdA, TAH, FYCM), pp. 186–201.
CAV-2000-VogeJ #algorithm #game studies
A Discrete Strategy Improvement Algorithm for Solving Parity Games (JV, MJ), pp. 202–215.
CAV-2000-BehrmannHV #how #matter #model checking #order
Distributing Timed Model Checking — How the Search Order Matters (GB, TH, FWV), pp. 216–231.
CAV-2000-EsparzaHRS #algorithm #automaton #model checking #performance
Efficient Algorithms for Model Checking Pushdown Systems (JE, DH, PR, SS), pp. 232–247.
CAV-2000-SomenziB #automaton #ltl #performance
Efficient Büchi Automata from LTL Formulae (FS, RB), pp. 248–263.
CAV-2000-StollerUL #detection #distributed #partial order #performance #using
Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods (SDS, LU, YAL), pp. 264–279.
CAV-2000-AlurGM #analysis #performance #reachability
Efficient Reachability Analysis of Hierarchical Reactive Machines (RA, RG, MM), pp. 280–295.
CAV-2000-Velev #execution #verification
Formal Verification of VLIW Microprocessors with Speculative Execution (MNV), pp. 296–311.
CAV-2000-McMillanQS #composition #induction #model checking
Induction in Compositional Model Checking (KLM, SQ, JBS), pp. 312–327.
CAV-2000-PnueliS #liveness #verification
Liveness and Acceleration in Parameterized Verification (AP, ES), pp. 328–343.
CAV-2000-RusinowitchSK #consistency #incremental #verification
Mechanical Verification of an Ideal Incremental ABR Conformance (MR, SS, FK), pp. 344–357.
CAV-2000-BaierHHK #analysis #markov #model checking
Model Checking Continuous-Time Markov Chains by Transient Analysis (CB, BRH, HH, JPK), pp. 358–372.
CAV-2000-CassezL #constraints #hybrid #model checking
Model-Checking for Hybrid Systems by Quotienting and Constraints Solving (FC, FL), pp. 373–388.
CAV-2000-FraerKZVF #analysis #performance #reachability #traversal #verification
Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification (RF, GK, BZ, MYV, LF), pp. 389–402.
CAV-2000-BouajjaniJNT #model checking
Regular Model Checking (AB, BJ, MN, TT), pp. 403–418.
CAV-2000-AnnichiniAB #parametricity #reasoning
Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems (AA, EA, AB), pp. 419–434.
CAV-2000-NamjoshiK #abstraction #automation #program transformation
Syntactic Program Transformations for Automatic Abstraction (KSN, RPK), pp. 435–449.
CAV-2000-Chan #query
Temporal-Locig Queries (WC), pp. 450–463.
CAV-2000-BouyerDFP #automaton #question
Are Timed Automata Updatable? (PB, CD, EF, AP), pp. 464–479.
CAV-2000-Shtrichman #bound #model checking #satisfiability
Tuning SAT Checkers for Bounded Model Checking (OS), pp. 480–494.
CAV-2000-AbdullaIN #bound #petri net
Unfoldings of Unbounded Petri Nets (PAA, SPI, AN), pp. 495–507.
CAV-2000-Rushby #diagrams #invariant #verification
Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification (JMR), pp. 508–520.
CAV-2000-HosabettuGS #architecture #exception #verification
Verifying Advanced Microarchitectures that Support Speculation and Exceptions (RH, GG, MKS), pp. 521–537.
CAV-2000-AbarbanelBGKW #automation #generative #named #simulation #specification
FoCs: Automatic Generation of Simulation Checkers from Formal Specifications (YA, IB, LG, SK, YW), pp. 538–542.
CAV-2000-BozgaFGGKM #named #validation
IF: A Validation Environment for Timed Asynchronous Systems (MB, JCF, LG, SG, JPK, LM), pp. 543–547.
CAV-2000-OwreR
Integrating WS1S with PVS (SO, HR), pp. 548–551.
CAV-2000-GunterKP #interactive #named #testing
PET: An Interactive Software Testing Tool (ELG, RPK, DP), pp. 552–556.
CAV-2000-ColbyLN #architecture #java
A Proof-Carrying Code Architecture for Java (CC, PL, GCN), pp. 557–560.
CAV-2000-BienmullerDW #verification
The STATEMATE Verification Environment — Making It Real (TB, WD, HW), pp. 561–567.
CAV-2000-Cohen #encryption #first-order #named #protocol #verification
TAPS: A First-Order Verifier for Cryptographic Protocols (EC), pp. 568–571.
CAV-2000-Yoneda #named #verification
VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits (TY), pp. 572–575.
CAV-2000-RamakrishnanRSDDRV #named #tool support #verification
XMC: A Logic-Programming-Based Verification Toolset (CRR, IVR, SAS, YD, XD, AR, VNV), pp. 576–580.

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.