Alan J. Hu, Moshe Y. Vardi
Proceedings of the 10th International Conference on Computer Aided Verification
CAV, 1998.

@proceedings{CAV-1998,
	address       = "Vancouver, British Columbia, Canada",
	editor        = "Alan J. Hu and Moshe Y. Vardi",
	isbn          = "3-540-64608-6",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 10th International Conference on Computer Aided Verification}",
	volume        = 1427,
	year          = 1998,
}

Event page: http://www.cs.ubc.ca/~ajh/cav98.html

Contents (54 items)

17 ×#verification
14 ×#model checking
7 ×#using
5 ×#proving
4 ×#design
4 ×#formal method
4 ×#multi
4 ×#named
4 ×#protocol
4 ×#realtime

CAV-1998-Halbwachs #programming

Synchronous Programming of Reactive Systems (NH), pp. 1–16.

CAV-1998-Peled #partial order #reduction

Ten Years of Partial Order Reduction (DP), pp. 17–28.

CAV-1998-Moore #proving

An ACL2 Proof of Write Invalidate Cache Coherence (JSM), pp. 29–38.

CAV-1998-HardinWG #concept #design #proving #theorem proving

Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle (DSH, MW, DAG), pp. 39–44.

CAV-1998-Camilleri #design #multi #proving #theorem proving

A Role for Theorem Proving in Multi-Processor Design (AJC), pp. 45–48.

CAV-1998-HoffmanP #experience #formal method

A Formal Method Experience at Secure Computing Corporation (JH, CP), pp. 49–56.

CAV-1998-Cuellar #formal method #industrial

Formal Methods in an Industrial Environment (JC), pp. 57–60.

CAV-1998-Holzmann #model checking #on the

On Checking Model Checkers (GJH), pp. 61–70.

CAV-1998-Mitchell #analysis #finite #protocol #security

Finite-State Analysis of Security Protocols (JCM), pp. 71–76.

CAV-1998-Bolignano #encryption #model checking #protocol #verification

Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols (DB), pp. 77–87.

CAV-1998-WolperB #infinity #verification

Verifying Systems with Infinite but Regular State Spaces (PW, BB), pp. 88–97.

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-McMillan #algorithm #composition #implementation #model checking #verification

Verification of an Implementation of Tomasulo’s Algorithm by Compositional Model Checking (KLM), pp. 110–121.

CAV-1998-HosabettuSG #correctness #pipes and filters #proving

Decomposing the Proof of Correctness of pipelined Microprocessors (RH, MKS, GG), pp. 122–134.

CAV-1998-SawadaH #execution #precise #verification

Processor Verification with Precise Exeptions and Speculative Execution (JS, WAHJ), pp. 135–146.

CAV-1998-ClarkeEJS #model checking #reduction #symmetry

Symmetry Reductions inModel Checking (EMC, EAE, SJ, APS), pp. 147–158.

CAV-1998-MankuHB #model checking #symmetry

Structural Symmetry and Model Checking (GSM, RH, RKB), pp. 159–171.

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.

CAV-1998-BeerBL #model checking #on the fly

On-the-Fly Model Checking of RCTL Formulas (IB, SBD, AL), pp. 184–194.

CAV-1998-HenzingerKQ #model checking

From Pre-historic to Post-modern Symbolic Model Checking (TAH, OK, SQ), pp. 195–206.

CAV-1998-Wallner #ltl #model checking #using

Model Checking LTL Using Net Unforldings (FW), pp. 207–218.

CAV-1998-XuCSCM #first-order #graph #logic #model checking #multi #using

Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs (YX, EC, XS, FC, OAM), pp. 219–231.

CAV-1998-Thathachar #on the #order

On the Limitations of Ordered Representations of Functions (JST), pp. 232–243.

CAV-1998-GoelSZAS #formal method #similarity

BDD Based Procedures for a Theory of Equality with Uninterpreted Functions (AG, KS, HZ, AA, VS), pp. 244–255.

CAV-1998-IslesHB #infinity #memory management

Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory (AJI, RH, RKB), pp. 256–267.

CAV-1998-ComonJ #analysis #automaton #multi #safety

Multiple Counters Automata, Safety Analysis and Presburger Arithmetic (HC, YJ), pp. 268–279.

CAV-1998-ShipleKR #comparison #reachability

A Comparison of Presburger Engines for EFSM Reachability (TRS, JHK, RKR), pp. 280–292.

CAV-1998-ColonU #abstraction #finite #generative #using

Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures (MC, TEU), pp. 293–304.

CAV-1998-AbdullaBJ #analysis #bound #on the fly

On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels (PAA, AB, BJ), pp. 305–318.

CAV-1998-BensalemLO #abstraction #automation #infinity

Computing Abstractions of Infinite State Systems Compositionally and Automatically (SB, YL, SO), pp. 319–331.

CAV-1998-GriffioenV #simulation

Normed Simulations (WODG, FWV), pp. 332–344.

CAV-1998-CourturierM #empirical #formal method #using

An Experiment in Parallelizing an Application Using Formal Methods (RC, DM), pp. 345–356.

CAV-1998-StollerL #detection #distributed #performance

Efficient Symbolic Detection of Global Properties in Distributed Systems (SDS, YAL), pp. 357–368.

CAV-1998-Wilding #policy #proving #realtime #scheduling

A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy (MW), pp. 369–378.

CAV-1998-AbdullaJKP #approach #partial order #reduction #verification

A General Approach to Partial Order Reductions in Symbolic Verification (PAA, BJ, MK, DP), pp. 379–390.

CAV-1998-Balarin #approach #concurrent #correctness #modelling #verification

Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models (FB), pp. 391–402.

CAV-1998-BelluominiM #using #verification

Verification of Timed Systems Using POSETs (WB, CJM), pp. 403–415.

CAV-1998-BellaP #induction

Mechanising BAN Kerberos by the Inductive Method (GB, LCP), pp. 416–427.

CAV-1998-FeltyHS #protocol #verification

Protocol Verification in Nuprl (APF, DJH, FAS), pp. 428–439.

CAV-1998-HenzingerQR #case study

You Assume, We Guarantee: Methodology and Case Studies (TAH, SQ, SKR), pp. 440–451.

CAV-1998-EmersonN #protocol #verification

Verification of Parameterized Bus Arbitration Protocol (EAE, KSN), pp. 452–463.

CAV-1998-NalumasuGMG #approach #memory management #model checking #modelling #multi #verification

The “Test Model-Checking” Approach to the Verification of Formal Memory Models of Multiprocessors (RN, RG, AM, GG), pp. 464–476.

CAV-1998-KaufmannMP #constraints #design #model checking

Design Constraints in Symbolic Model Checking (MK, AM, CP), pp. 477–487.

CAV-1998-ChenB #float #verification

Verification of Floating-Point Adders (YAC, REB), pp. 488–499.

CAV-1998-Bouali #verification

XEVE, an ESTEREL Verification Environment (AB), pp. 500–504.

CAV-1998-BensalemLO98a #invariant #named #verification

InVeST: A Tool for the Verification of Invariants (SB, YL, SO), pp. 505–510.

CAV-1998-FerrariGMPR #mobile #process #verification

Verifying Mobile Processes in the HAL Environment (GLF, SG, UM, MP, GR), pp. 511–515.

CAV-1998-ElgaardKM

MONA 1.x: New Techniques for WS1S and WS2S (JE, NK, AM), pp. 516–520.

CAV-1998-AlurHMQRT #composition #model checking #named

MOCHA: Modularity in Model Checking (RA, TAH, FYCM, SQ, SKR, ST), pp. 521–525.

CAV-1998-HeitmeyerKLB #requirements #specification #tool support

SCR*: A Toolset for Specifying and Analyzing Software Requirements (CLH, JK, BGL, RB), pp. 526–531.

CAV-1998-Peled98a #sequence chart #tool support

A Toolset for Message Sequence Charts (DP), pp. 532–536.

CAV-1998-BrockmeyerW #design #realtime #verification

Real-Time Verification of Statemate Designs (UB, GW), pp. 537–541.

CAV-1998-Daws #model checking #named #realtime

Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems (CD), pp. 542–545.

CAV-1998-BozgaDMOTY #model checking #named #realtime

Kronos: A Model-Checking Tool for Real-Time Systems (MB, CD, OM, AO, ST, SY), pp. 546–550.