Susanne Graf, Michael I. Schwartzbach
Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS, 2000.

@proceedings{TACAS-2000,
	address       = "Berlin, Germany",
	editor        = "Susanne Graf and Michael I. Schwartzbach",
	isbn          = "3-540-67282-6",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems}",
	volume        = 1785,
	year          = 2000,
}

Contents (36 items)

8 ×#model checking
6 ×#verification
4 ×#named
4 ×#using
3 ×#constraints
3 ×#generative
3 ×#on the
3 ×#tool support
2 ×#analysis
2 ×#automation

TACAS-2000-WolperB #automaton #constraints #linear #on the

On the Construction of Automata from Linear Arithmetic Constraints (PW, BB), pp. 1–19.

TACAS-2000-XiongL #component #design #type system

An Extensible Type System for Component-Based Design (YX, EAL), pp. 20–37.

TACAS-2000-Aspinall #development #proving

Proof General: A Generic Tool for Proof Development (DA0), pp. 38–42.

TACAS-2000-GoedickeEMT #development #distributed #graph transformation #multi #tool support

ViewPoint-Oriented Software Development: Tool Support for Integrating Multiple Perspectives by Distributed Graph Transformation (MG, BE, TM, GT), pp. 43–47.

TACAS-2000-BraunLSS #consistency #formal method #integration

Consistent Integration of Formal Methods (PB, HL, BS, OS), pp. 48–62.

TACAS-2000-MeyerP #architecture #interactive #proving

An Architecture for Interactive Program Provers (JM, APH), pp. 63–77.

TACAS-2000-DennisCNBSRGM #tool support

The PROSPER Toolkit (LAD, GC, MN, RJB, KS, GR, MJCG, TFM), pp. 78–92.

TACAS-2000-Mossakowski #named #semantics #tool support

CASL: From Semantics to Tools (TM), pp. 93–108.

TACAS-2000-BornotGS #on the

On the Construction of Live Timed Systems (SB, GG, JS), pp. 109–126.

TACAS-2000-LarssonPY #model checking #on the #problem #traversal

On Memory-Block Traversal Problems in Model-Checking Timed-Systems (FL, PP, WY), pp. 127–141.

TACAS-2000-HenzingerM #hybrid #model checking

Symbolic Model Checking for Rectangular Hybrid Systems (TAH, RM), pp. 142–156.

TACAS-2000-Wang #data type #performance #realtime #verification

Efficient Data Structure for Fully Symbolic Verification of Real-Time Software Systems (FW), pp. 157–171.

TACAS-2000-RoychoudhuryKRRS #logic programming #program transformation #using #verification

Verification of Parameterized Systems Using Logic Program Transformations (AR, KNK, CRR, IVR, SAS), pp. 172–187.

TACAS-2000-BaukusBLS #network #verification

Abstracting WS1S Systems to Verify Parameterized Networks (KB, SB, YL, KS), pp. 188–203.

TACAS-2000-BodeveixF #infinity #named #validation

FMona: A Tool for Expressing Validation Techniques over Infinite State Systems (JPB, MF), pp. 204–219.

TACAS-2000-JonssonN #infinity #transitive #verification

Transitive Closures of Regular Relations for Verifying Infinite-State Systems (BJ, MN), pp. 220–234.

TACAS-2000-BozgaFG #automation #generative #static analysis #testing #using

Using Static Analysis to Improve Automatic Test Generation (MB, JCF, LG), pp. 235–250.

TACAS-2000-Mateescu #equation #generative #performance

Efficient Diagnostic Generation for Boolean Equation Systems (RM), pp. 251–265.

TACAS-2000-KrimmM #communication #composition #generative #partial order #reduction

Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems (JPK, LM), pp. 266–282.

TACAS-2000-HelovuoV #process

Checking for CFFD-Preorder with Tester Processes (JH, AV), pp. 283–298.

TACAS-2000-HenzingerR #bisimulation

Fair Bisimulation (TAH, SKR), pp. 299–314.

TACAS-2000-Schmidt #analysis #low level #reachability #symmetry

Integrating Low Level Symmetries into Reachability Analysis (KS0), pp. 315–330.

TACAS-2000-CastilloW #model checking

Model Checking Support for the ASM High-Level Language (GDC, KW), pp. 331–346.

TACAS-2000-HermannsKMS #markov #model checking

A Markov Chain Model Checker (HH, JPK, JMK, MS), pp. 347–362.

TACAS-2000-BosnackiDHS #model checking

Model Checking SDL with Spin (DB, DD, LH, NS), pp. 363–377.

TACAS-2000-BharadwajS #automation #constraints #invariant #named #theorem proving

Salsa: Combining Constraint Solvers with BDDs for Automatic Invariant Checking (RB, SS), pp. 378–394.

TACAS-2000-AlfaroKNPS #model checking #probability #process #representation #using

Symbolic Model Checking of Probabilistic Processes Using MTBDDs and the Kronecker Representation (LdA, MZK, GN, DP, RS), pp. 395–410.

TACAS-2000-AbdullaBE #analysis #reachability

Symbolic Reachability Analysis Based on SAT-Solvers (PAA, PB, NE), pp. 411–425.

TACAS-2000-DelzannoR #representation #set

Symbolic Representation of Upward-Closed Sets (GD, JFR), pp. 426–440.

TACAS-2000-Bultan #concurrent #constraints #evaluation #model checking

BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems (TB), pp. 441–455.

TACAS-2000-NiemannB #editing #specification #visual notation

Tool-Based Specification of Visual Languages and Graphic Editors (MN, RB), pp. 456–470.

TACAS-2000-KamelL #compilation #editing #named #visual notation

VIP: A Visual Editor and Compiler for v-Promela (MK, SL), pp. 471–486.

TACAS-2000-AronsP #comparison #execution #verification

A Comparison of Two Verification Methods for Speculative Instruction Execution (TA, AP), pp. 487–502.

TACAS-2000-ClarkeJM #partial order #protocol #reduction #security #verification

Partial Order Reductions for Security Protocol Verification (EMC, SJ, WRM), pp. 503–518.

TACAS-2000-BenerecettiG #logic #model checking #protocol #security #using

Model Checking Security Protocols Using a Logic of Belief (MB, FG), pp. 519–534.

TACAS-2000-GnesiLLAAM #fault #specification #validation

A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors (SG, DL, GL, CA, AMA, PM), pp. 535–549.