Tiziana Margaria-Steffen, Wang Yi
Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS, 2001.
@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.
9 ×#model checking
6 ×#verification
4 ×#abstraction
4 ×#analysis
4 ×#automaton
4 ×#testing
4 ×#using
3 ×#automation
3 ×#generative
3 ×#linear
6 ×#verification
4 ×#abstraction
4 ×#analysis
4 ×#automaton
4 ×#testing
4 ×#using
3 ×#automation
3 ×#generative
3 ×#linear