BibSLEIGH — Proceedings of the Ninth International Conference on Computer Aided Verification

Orna Grumberg
Proceedings of the Ninth International Conference on Computer Aided Verification
CAV, 1997.

TEST

@proceedings{CAV-1997,
	address       = "Haifa, Israel",
	editor        = "Orna Grumberg",
	isbn          = "3-540-63166-6",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Ninth International Conference on Computer Aided Verification}",
	volume        = 1254,
	year          = 1997,
}

Contents (52 items)

CAV-1997-Marschner #challenge #industrial #tool support #verification: Practical Challenges for Industrial Formal Verification Tools (FEM), pp. 1–2.
CAV-1997-Hughes #approach #verification: Formal Verification of Digital Systems, from ASICs to HW/SW Codesign — a Pragmatic Approach (RBH), pp. 3–6.
CAV-1997-Boralv #industrial #tool support #verification: The Industrial Success of Verification Tools Based on Stålmarck’s Method (AB), pp. 7–10.
CAV-1997-Rowe #case study #verification: Formal Verification — Applications & Case Studies (MR), p. 11.
CAV-1997-PardoH #abstraction #automation #calculus #model checking #μ-calculus: Automatic Abstraction Techniques for Propositional μ-calculus Model Checking (AP, GDH), pp. 12–23.
CAV-1997-McMillan #composition #design #hardware #refinement: A Compositional Rule for Hardware Design Refinement (KLM), pp. 24–35.
CAV-1997-KupfermanV #revisited: Module Checking Revisited (OK, MYV), pp. 36–47.
CAV-1997-Kaivola #composition #using #verification: Using Compositional Preorders in the Verification of Sliding Window Protocal (RK), pp. 48–59.
CAV-1997-CyrlukMR #formal method #performance: An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors (DC, MOM, HR), pp. 60–71.
CAV-1997-GrafS #graph: Construction of Abstract State Graphs with PVS (SG, HS), pp. 72–83.
CAV-1997-TurkPP #process #testing #verification: Verification of a Chemical Process Leak Test Procedure (ALT, STP, GJP), pp. 84–94.
CAV-1997-KamhiWF #automation #performance: Automatic Datapath Extraction for Efficient Usage of HDD (GK, OW, LF), pp. 95–106.
CAV-1997-Klarlund #algorithm #online #refinement: An n log n Algorithm for Online BDD Refinement (NK), pp. 107–118.
CAV-1997-BaierH #bisimulation #probability #process: Weak Bisimulation for Fully Probabilistic Processes (CB, HH), pp. 119–130.
CAV-1997-Bolignano #encryption #towards #verification: Towards a Mechanization of Cryptographic Protocal Verification (DB), pp. 131–142.
CAV-1997-RamakrishnanRRSSW #model checking #performance #using: Efficient Model Checking Using Tabled Resolution (YSR, CRR, IVR, SAS, TS, DSW), pp. 143–154.
CAV-1997-Fisler #decidability #diagrams #regular expression: Containing of Regular Languages in Non-Regular Timing Diagram Languages is Decidable (KF), pp. 155–166.
CAV-1997-BoigelotBR #analysis #hybrid #linear #reachability: An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (BB, LB, SR), pp. 167–178.
CAV-1997-BozgaMPY #automaton #verification: Some Progress in the Symbolic Verification of Timed Automata (MB, OM, AP, SY), pp. 179–190.
CAV-1997-TasiranB #case study #composition #named #verification: STARI: A Case Study in Compositional and Hierarchical Timing Verification (ST, RKB), pp. 191–201.
CAV-1997-CimattiGPPPRTY #certification #embedded #safety #verification: A Provably Correct Embedded Verifier for the Certification of Safety Critical Software (AC, FG, PP, BP, JP, DR, PT, BY), pp. 202–213.
CAV-1997-BarrettM #design #model checking: Model Checking in a Microprocessor Design Project (GB, AM), pp. 214–225.
CAV-1997-Harel #years after: Some Thoughts on Statecharts, 13 Years Later (DH), pp. 226–231.
CAV-1997-GyurisS #model checking #on the fly #symmetry: On-the-Fly Model Checking Under Fairness That Exploits Symmetry (VG, APS), pp. 232–243.
CAV-1997-PandeyB #evaluation #symmetry #verification: Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation (MP, REB), pp. 244–255.
CAV-1997-SternD #verification: Parallelizing the Murphi Verifier (US, DLD), pp. 256–278.
CAV-1997-BeerBER #detection #performance: Efficient Detection of Vacuity in ACTL Formulaas (IB, SBD, CE, YR), pp. 279–290.
CAV-1997-ImmermanV #logic #model checking #transitive: Model Checking and Transitive-Closure Logic (NI, MYV), pp. 291–302.
CAV-1997-Berry #design #verification: Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous Design (GB), p. 303.
CAV-1997-CeceF #effectiveness #source code: Programs with Quasi-Stable Channels are Effectively Recognizable (GC, AF), pp. 304–315.
CAV-1997-ChanABN #constraints #model checking #theorem proving: Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints (WC, RJA, PB, DN), pp. 316–327.
CAV-1997-KokkarinenPV #partial order #reduction: Relaxed Visibility Enhances Partial Order Reduction (IK, DP, AV), pp. 328–339.
CAV-1997-AlurBHQR #partial order #reduction: Partial-Order Reduction in Symbolic State Space Exploration (RA, RKB, TAH, SQ, SKR), pp. 340–351.
CAV-1997-MelzerR #concurrent #using: Deadlock Checking Using Net Unfoldings (SM, SR), pp. 352–363.
CAV-1997-SawadaH #approach #pipes and filters #verification: Trace Table Based Approach for Pipeline Microprocessor Verification (JS, WAHJ), pp. 364–375.
CAV-1997-YuanSAA #on the #verification: On Combining Formal and Informal Verification (JY, JS, JAA, AA), pp. 376–387.
CAV-1997-VelevBJ #array #memory management #modelling #performance #simulation: Efficient Modeling of Memory Arrays in Symbolic Simulation (MNV, REB, AJ), pp. 388–399.
CAV-1997-BultanGP #infinity #model checking #using: Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic (TB, RG, WP), pp. 400–411.
CAV-1997-Sistla #automaton #invariant #linear #network #using #verification: Parametrized Verification of Linear Networks Using Automata as Invariants (APS), pp. 412–423.
CAV-1997-KestenMMPS #model checking: Symbolic Model Checking with Rich ssertional Languages (YK, OM, MM, AP, ES), pp. 424–435.
CAV-1997-Saidi #automation #deduction #invariant #verification: The Invariant Checker: Automated Deductive Verification of Reactive Systems (HS), pp. 436–439.
CAV-1997-Grahlmann: The PEP Tool (BG), pp. 440–443.
CAV-1997-LindenstraussSS #logic programming #named #query #source code #termination: TermiLog: A System for Checking Termination of Queries to Logic Programs (NL, YS, AS), pp. 444–447.
CAV-1997-KelbMMG #named #performance: MOSEL: A Sound and Efficient Tool for M2L(Str) (PK, TMS, MM, CG), pp. 448–451.
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.
CAV-1997-LarsenPY #named: UPPAAL: Status & Developments (KGL, PP, WY), pp. 456–459.
CAV-1997-HenzingerHW #hybrid #model checking #named: HYTECH: A Model Checker for Hybrid Systems (TAH, PHH, HWT), pp. 460–463.
CAV-1997-SistlaMG #liveness #model checking #named #symmetry #verification: SMC: A Symmetry Based Model Checker for Verification of Liveness Properties (APS, LM, VG), pp. 464–467.
CAV-1997-Biere #calculus #model checking #named #performance #μ-calculus: μcke — Efficient μ-Calculus Model Checking (AB), pp. 468–471.
CAV-1997-VarpaaniemiHL #analysis #performance #reachability: prod 3.2: An Advanced Tool for Efficient Reachability Analysis (KV, KH, JL), pp. 472–475.
CAV-1997-Godefroid #analysis #automation #concurrent #named: VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software (PG), pp. 476–479.
CAV-1997-BeerBEGGHLPRRW #model checking #named: RuleBase: Model Checking at IBM (IB, SBD, CE, DG, LG, TH, AL, PP, YR, GR, YW), pp. 480–483.

Orna GrumbergProceedings of the Ninth International Conference on Computer Aided VerificationCAV, 1997.

Contents (52 items)

Orna Grumberg
Proceedings of the Ninth International Conference on Computer Aided Verification
CAV, 1997.