Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems
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

Tiziana Margaria-Steffen, Wang Yi
Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS, 2001.

TCS
DBLP
Scholar
Full names Links ISxN
@proceedings{TACAS-2001,
	address       = "ETAPS 2001 Genova, Italy",
	editor        = "Tiziana Margaria-Steffen and Wang Yi",
	isbn          = "3-540-41865-2",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems}",
	volume        = 2031,
	year          = 2001,
}

Contents (41 items)

TACAS-2001-Vardi #branch #linear
Branching vs. Linear Time: Final Showdown (MYV), pp. 1–22.
TACAS-2001-Fourman #reasoning
Propositional Reasoning (MPF), p. 23.
TACAS-2001-Finkbeiner #nondeterminism
Language Containment Checking with Nondeterministic BDDs (BF), pp. 24–38.
TACAS-2001-WilliamsAH #diagrams #satisfiability #using
Satisfiability Checking Using Boolean Expression Diagrams (PFW, HRA, HH), pp. 39–51.
TACAS-2001-Yavuz-KahveciTB #library
A Library for Composite Symbolic Representations (TYK, MT, TB), pp. 52–66.
TACAS-2001-ColonS #linear #ranking #synthesis
Synthesis of Linear Ranking Functions (MC, HS), pp. 67–81.
TACAS-2001-PnueliRZ #automation #deduction #invariant #verification
Automatic Deductive Verification with Invisible Invariants (AP, SR, LDZ), pp. 82–97.
TACAS-2001-LakhnechBBO #abstraction #incremental #verification
Incremental Verification by Abstraction (YL, SB, SB, SO), pp. 98–112.
TACAS-2001-TiwariRSS #generative #invariant
A Technique for Invariant Generation (AT, HR, HS, NS), pp. 113–127.
TACAS-2001-SebastianiTG #model checking #student
Model Checking Syllabi and Student Carreers (RS, AT, FG), pp. 128–142.
TACAS-2001-FuBHS #verification #workflow
Verification of Vortex Workflows (XF, TB, RH, JS), pp. 143–157.
TACAS-2001-BallCR #library #parallel #thread #verification
Parameterized Verification of Multithreaded Software Libraries (TB, SC, SKR), pp. 158–173.
TACAS-2001-BehrmannF #performance #towards
Efficient Guiding Towards Cost-Optimality in UPPAAL (GB, AF), pp. 174–188.
TACAS-2001-HuneRSV #automaton #linear #model checking #parametricity
Linear Parametric Model Checking of Timed Automata (TH, JR, MS, FWV), pp. 189–203.
TACAS-2001-AndovaB #abstraction #algebra #probability #process
Abstraction in Probabilistic Process Algebra (SA, JCMB), pp. 204–219.
TACAS-2001-RuysLKLM #algebra #analysis #partial order #probability #process #using
First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders (TCR, RL, JPK, DL, MM), pp. 220–235.
TACAS-2001-MycroftS #co-evolution #design #functional #hardware #using
Hardware/Software Co-Design Using Functional Languages (AM, RS), pp. 236–251.
TACAS-2001-Velev #abstraction #automation #verification
Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors (MNV), pp. 252–267.
TACAS-2001-BallPR #abstraction #c #model checking #source code
Boolean and Cartesian Abstraction for Model Checking C Programs (TB, AP, SKR), pp. 268–283.
TACAS-2001-PasareanuDV #java #model checking #source code
Finding Feasible Counter-examples when Model Checking Abstracted Java Programs (CSP, MBD, WV), pp. 284–298.
TACAS-2001-BergJ #compilation #java #ml
The LOOP Compiler for Java and JML (JvdB, BJ), pp. 299–312.
TACAS-2001-CimattiRB #automaton #model checking #set
Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking (AC, MR, PB), pp. 313–327.
TACAS-2001-CiardoLS #generative #named #performance
Saturation: An Efficient Iteration Strategy for Symbolic State-Space Generation (GC, GL, RS), pp. 328–342.
TACAS-2001-NielsenS #automation #automaton #generative #testing
Automated Test Generation from Timed Automata (BN, AS), pp. 343–357.
TACAS-2001-Khurshid #algorithm #search-based #testing #using
Testing an Intentional Naming Scheme Using Genetic Algorithms (SK), pp. 358–372.
TACAS-2001-RiccaT #analysis #problem #testing #web
Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions (FR, PT), pp. 373–388.
TACAS-2001-SouterWSP #analysis #named #testing
TATOO: Testing and Analysis Tool for Object- Oriented Software (ALS, TMW, SAS, LLP), pp. 389–403.
TACAS-2001-ChechikDE #implementation #model checking #multi
Implementing a Multi-valued Symbolic Model Checker (MC, BD, SME), pp. 404–419.
TACAS-2001-FislerFVY #algorithm #detection #question
Is There a Best Symbolic Cycle-Detection Algorithm? (KF, RF, GK, MYV, ZY), pp. 420–434.
TACAS-2001-Carvajal-SchiaffinoDC #bound #petri net #validation
Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets (RCS, GD, GC), pp. 435–449.
TACAS-2001-ChristensenKM
A Sweep-Line Method for State Space Exploration (SC, LMK, TM), pp. 450–464.
TACAS-2001-AmlaENT #composition #diagrams #reasoning
Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams (NA, EAE, KSN, RJT), pp. 465–479.
TACAS-2001-TanC #revisited #simulation
Simulation Revisited (LT, RC), pp. 480–495.
TACAS-2001-GunterMP #composition #sequence chart
Compositional Message Sequence Charts (ELG, AM, DP), pp. 496–511.
TACAS-2001-KloseW #automaton #sequence chart
An Automata Based Interpretation of Live Sequence Charts (JK, HW), pp. 512–527.
TACAS-2001-ChocklerKV #logic #metric #model checking
Coverage Metrics for Temporal Logic Model Checking (HC, OK, MYV), pp. 528–542.
TACAS-2001-BolligLW #calculus #model checking #parallel #μ-calculus
Parallel Model Checking for the Alternation Free μ-Calculus (BB, ML, MW), pp. 543–558.
TACAS-2001-Pandya #model checking
Model Checking CTL*[DC] (PKP), pp. 559–573.
TACAS-2001-Beaudouin-LafonMJAJLLMMRRCJ #editing #named #petri net #simulation #tool support
CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS (MBL, WEM, MJ, PA, PJ, HML, KL, KHM, SM, AVR, KR, SC, KJ), pp. 574–577.
TACAS-2001-Castillo #analysis #modelling #state machine #tool support #validation
The ASM Workbench — A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models Tool Demonstration (GDC), pp. 578–581.
TACAS-2001-NollFG #erlang #verification
The Erlang Verification Tool (TN, LÅF, DG), pp. 582–586.

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.