BibSLEIGH — Proceedings of the 13th International Conference on Computer Aided Verification

Gérard Berry, Hubert Comon, Alain Finkel
Proceedings of the 13th International Conference on Computer Aided Verification
CAV, 2001.

TEST

@proceedings{CAV-2001,
	address       = "Paris, France",
	editor        = "Gérard Berry and Hubert Comon and Alain Finkel",
	isbn          = "3-540-42345-1",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 13th International Conference on Computer Aided Verification}",
	volume        = 2102,
	year          = 2001,
}

Event page: http://www.lsv.ens-cachan.fr/Events/cav01/

Contents (48 items)

CAV-2001-Parnas #documentation #process #verification: Software Documentation and the Verification Process (DLP), p. 1.
CAV-2001-Namjoshi #model checking: Certifying Model Checkers (KSN), pp. 2–13.
CAV-2001-Bertot #formal method #proving #theorem proving #verification: Formalizing a JVML Verifier for Initialization in a Theorem Prover (YB), pp. 14–24.
CAV-2001-RoychoudhuryR #automation #induction #protocol #verification: Automated Inductive Verification of Parameterized Protocols (AR, IVR), pp. 25–37.
CAV-2001-BhatCG #automaton #model checking #performance: Efficient Model Checking Via Büchi Tableau Automata (GB, RC, AG), pp. 38–52.
CAV-2001-GastinO #automaton #ltl #performance: Fast LTL to Büchi Automata Translation (PG, DO), pp. 53–65.
CAV-2001-ChocklerKKV #approach #model checking: A Practical Approach to Coverage in Model Checking (HC, OK, RPK, MYV), pp. 66–78.
CAV-2001-DovierPP #algorithm #bisimulation #performance: A Fast Bisimulation Algorithm (AD, CP, AP), pp. 79–90.
CAV-2001-SistlaG #model checking #symmetry: Symmetry and Reduced Symmetry in Model Checking (APS, PG), pp. 91–103.
CAV-2001-KuehlmannB #using #verification: Transformation-Based Verification Using Generalized Retiming (AK, JB), pp. 104–117.
CAV-2001-Cabodi #named #representation: Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions (GC), pp. 118–130.
CAV-2001-MoondanosSHK #divide and conquer #equivalence #logic #named #verification: CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination (JM, CJHS, ZH, DK), pp. 131–143.
CAV-2001-RodehS #equivalence #finite #logic: Finite Instantiations in Equivalence Logic with Uninterpreted Functions (YR, OS), pp. 144–154.
CAV-2001-AsterothBA #model checking #modelling: Model Checking with Formula-Dependent Abstract Models (AA, CB, UA), pp. 155–168.
CAV-2001-AlurW #implementation #network #protocol #refinement #verification: Verifying Network Protocol Implementations by Symbolic Refinement Checking (RA, BYW), pp. 169–181.
CAV-2001-ZhengMM #abstraction #automation #verification: Automatic Abstraction for Verification of Timed Circuits and Systems (HZ, EM, CJM), pp. 182–193.
CAV-2001-KwiatkowskaNS #automation #distributed #protocol #random #using #verification: Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM (MZK, GN, RS), pp. 194–206.
CAV-2001-AlurEY #analysis #recursion #state machine: Analysis of Recursive State Machines (RA, KE, MY), pp. 207–220.
CAV-2001-AronsPRXZ #automation #induction #verification: Parameterized Verification with Automatically Computed Inductive Assertions (TA, AP, SR, JX, LDZ), pp. 221–234.
CAV-2001-VelevB #logic #named #similarity: EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations (MNV, REB), pp. 235–240.
CAV-2001-SongPP #automation #generative #implementation #named #protocol #security #verification: AGVI — Automatic Generation, Verification, and Implementation of Security Protocols (DXS, AP, DP), pp. 241–245.
CAV-2001-FilliatreORS #named: ICS: Integrated Canonizer and Solver (JCF, SO, HR, NS), pp. 246–249.
CAV-2001-BlomFGLLP #algebra #named #specification #tool support: µCRL: A Toolset for Analysing Algebraic Specifications (SB, WF, JFG, IvL, BL, JvdP), pp. 250–254.
CAV-2001-LeuckerN #concurrent #framework #named #parallel #platform #verification: Truth/SLC — A Parallel Verification Platform for Concurrent Systems (ML, TN), pp. 255–259.
CAV-2001-BallR #tool support: The SLAM Toolkit (TB, SKR), pp. 260–264.
CAV-2001-Leroy #bytecode #java #overview #perspective #verification: Java Bytecode Verification: An Overview (XL), pp. 265–285.
CAV-2001-DamsLS #transducer: Iterating Transducers (DD, YL, MS), pp. 286–297.
CAV-2001-DelzannoRB #explosion: Attacking Symbolic State Explosion (GD, JFR, LVB), pp. 298–310.
CAV-2001-Maidl #approach #model checking #safety: A Unifying Model Checking Approach for Safety Properties of Parameterized Systems (MM), pp. 311–323.
CAV-2001-EsparzaS #model checking #recursion #source code: A BDD-Based Model Checker for Recursive Programs (JE, SS), pp. 324–336.
CAV-2001-Alfaro #model checking #web: Model Checking the World Wide Web (LdA), pp. 337–349.
CAV-2001-GrumbergHS #calculus #distributed #model checking #μ-calculus: Distributed Symbolic Model Checking for μ-Calculus (OG, TH, AS), pp. 350–362.
CAV-2001-BeerBEFGR #logic: The Temporal Logic Sugar (IB, SBD, CE, DF, AG, YR), pp. 363–367.
CAV-2001-AnnichiniBS #analysis #named #reachability: TReX: A Tool for Reachability Analysis of Complex Systems (AA, AB, MS), pp. 368–372.
CAV-2001-JohannsenB #design #named: BooStER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstarction (PJ), pp. 373–377.
CAV-2001-LevinY #model checking #named: SDLcheck: A Model Checking Tool (VL, HY), p. 377.
CAV-2001-ShanbhagGTAL #model checking #named: EASN: Integrating ASN.1 and Model Checking (VKS, KG, MT, AA, ML), pp. 382–386.
CAV-2001-AmlaEKN #diagrams #model checking #named #performance: Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams (NA, EAE, RPK, KSN), pp. 387–390.
CAV-2001-ClossePPSVWY #development #embedded #named #realtime #verification: TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems (EC, MP, JP, JS, PV, DW, SY), pp. 391–395.
CAV-2001-JhalaM #architecture #composition #model checking #verification: Microarchitecture Verification by Compositional Model Checking (RJ, KLM), pp. 396–410.
CAV-2001-Moore #execution #modelling #state machine #symbolic computation: Rewriting for Symbolic Execution of State Machine Models (JSM), pp. 411–422.
CAV-2001-Arons #consistency #using #verification: Using Timestamping and History Variables to Verify Sequential Consistency (TA), pp. 423–435.
CAV-2001-CoptyFFGKTV #bound #industrial #model checking: Benefits of Bounded Model Checking at an Industrial Setting (FC, LF, RF, EG, GK, AT, MYV), pp. 436–453.
CAV-2001-BjesseLM #debugging #satisfiability #using: Finding Bugs in an α Microprocessor Using Satisfiability Solvers (PB, TL, AM), pp. 454–464.
CAV-2001-MoriokaKY #algorithm #performance #towards #verification: Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m) (SM, YK, TY), pp. 465–477.
CAV-2001-AbdeddaimM #automaton #scheduling #using: Job-Shop Scheduling Using Timed Automata (YA, OM), pp. 478–492.
CAV-2001-LarsenBBFHPR #automaton #performance #reachability: As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata (KGL, GB, EB, AF, TH, PP, JR), pp. 493–505.
CAV-2001-Dang #analysis #automaton #reachability: Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks (ZD), pp. 506–518.

Gérard Berry, Hubert Comon, Alain FinkelProceedings of the 13th International Conference on Computer Aided VerificationCAV, 2001.

Event page: http://www.lsv.ens-cachan.fr/Events/cav01/

Contents (48 items)

Gérard Berry, Hubert Comon, Alain Finkel
Proceedings of the 13th International Conference on Computer Aided Verification
CAV, 2001.