Proceedings of the Ninth 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

Hubert Garavel, John Hatcliff
Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS, 2003.

TCS
DBLP
Scholar
Full names Links ISxN
@proceedings{TACAS-2003,
	address       = "Warsaw, Poland",
	editor        = "Hubert Garavel and John Hatcliff",
	isbn          = "3-540-00898-5",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems}",
	volume        = 2619,
	year          = 2003,
}

Contents (43 items)

TACAS-2003-Lee #case study #experience #what
What Are We Trying to Prove? Reflections on Experiences with Proof-Carrying Code (PL0), p. 1.
TACAS-2003-McMillanA #abstraction #automation
Automatic Abstraction without Counterexamples (KLM, NA), pp. 2–17.
TACAS-2003-BenedettiC #bound #ltl #model checking
Bounded Model Checking for Past LTL (MB, AC), pp. 18–33.
TACAS-2003-AmlaKMM #analysis #bound #model checking
Experimental Analysis of Different Techniques for Bounded Model Checking (NA, RPK, KLM, RM), pp. 34–48.
TACAS-2003-HenzingerKM #calculus #on the #μ-calculus
On the Universal and Existential Fragments of the μ-Calculus (TAH, OK, RM), pp. 49–64.
TACAS-2003-ArmoniBKV #linear #logic
Resets vs. Aborts in Linear Temporal Logic (RA, DB, OK, MYV), pp. 65–80.
TACAS-2003-Mateescu #equation #on the fly
A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems (RM), pp. 81–96.
TACAS-2003-FontaineG #decidability #invariant #validation
Decidability of Invariant Validation for Paramaterized Systems (PF, EPG), pp. 97–112.
TACAS-2003-ChkliaevHV #protocol #verification
Verification and Improvement of the Sliding Window Protocol (DC, JH, EPdV), pp. 113–127.
TACAS-2003-EsparzaM #multi #protocol
Simple Representative Instantiations for Multicast Protocols (JE, MM), pp. 128–143.
TACAS-2003-EmersonK #agile #model checking #protocol
Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols (EAE, VK), pp. 144–159.
TACAS-2003-GurfinkelC #proving
Proof-Like Counter-Examples (AG, MC), pp. 160–175.
TACAS-2003-GlusmanKMFV #abstraction #evaluation #industrial #multi #refinement
Multiple-Counterexample Guided Iterative Abstraction Refinement: An Industrial Evaluation (MG, GK, SMH, RF, MYV), pp. 176–191.
TACAS-2003-ClarkeFHKST #abstraction #hybrid #refinement #verification
Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement (EMC, AF, ZH, BHK, OS, MT), pp. 192–207.
TACAS-2003-AlurDI #abstraction #hybrid
Counter-Example Guided Predicate Abstraction of Hybrid Systems (RA, TD, FI), pp. 208–223.
TACAS-2003-FersmanMPY #analysis #scheduling #using
Schedulability Analysis Using Two Clocks (EF, LM, PP, WY), pp. 224–239.
TACAS-2003-AbdeddaimAM #nondeterminism #on the #scheduling
On Optimal Scheduling under Uncertainty (YA, EA, OM), pp. 240–253.
TACAS-2003-BehrmannBFL #analysis #automaton #verification
Static Guard Analysis in Timed Automata Verification (GB, PB, EF, KGL), pp. 254–277.
TACAS-2003-DembinskiJJPPSWZ #automaton #named #specification #verification
Verics: A Tool for Verifying Timed Automata and Estelle Specifications (PD, AJ, PJ, WP, AP, MS, BW, AZ), pp. 278–283.
TACAS-2003-BDSV #analysis #encryption #information management #protocol #representation
A New Knowledge Representation Strategy for Cryptographic Protocol Analysis (ICB, LD, RS, AV), pp. 284–298.
TACAS-2003-BozgaLP #abstraction #protocol #verification
Pattern-Based Abstraction for Verifying Secrecy in Protocols (LB, YL, MP), pp. 299–314.
TACAS-2003-BasuR #analysis #composition #verification
Compositional Analysis for Verification of Parameterized Systems (SB, CRR), pp. 315–330.
TACAS-2003-CobleighGP #composition #learning #verification
Learning Assumptions for Compositional Verification (JMC, DG, CSP), pp. 331–346.
TACAS-2003-Tripakis #automation #composition
Automated Module Composition (ST), pp. 347–362.
TACAS-2003-AlurTM #composition #game studies #graph #recursion
Modular Strategies for Recursive Game Graphs (RA, SLT, PM), pp. 363–378.
TACAS-2003-CiardoMS #bound
Saturation Unbound (GC, RMM, RS), pp. 379–393.
TACAS-2003-BartzisB #bound #constraints #performance
Construction of Efficient BDDs for Bounded Arithmetic Constraints (CB, TB), pp. 394–408.
TACAS-2003-SokolskyPLC #analysis #modelling #power management
Modeling and Analysis of Power-Aware Systems (OS, AP, IL, KC), pp. 409–425.
TACAS-2003-HermannsJ #analysis #component #dependence #performance #set
A Set of Performance and Dependability Analysis Components for CADP (HH, CJ), pp. 425–430.
TACAS-2003-ZhangCS #analysis #concurrent #functional #performance #verification
The Integrated CWB-NC/PIOATool for Functional Verification and Performance Analysis of Concurrent Systems (DZ, RC, EWS), pp. 431–436.
TACAS-2003-BraghinCFFLP #analysis #bound #named
BANANA — A Tool for Boundary Ambients Nesting ANAlysis (CB, AC, SF, RF, FLL, CP), pp. 437–441.
TACAS-2003-BerthomieuV #analysis #branch #petri net
State Class Constructions for Branching Analysis of Time Petri Nets (BB, FV), pp. 442–457.
TACAS-2003-KhomenkoK #branch #petri net #process
Branching Processes of High-Level Petri Nets (VK, MK), pp. 458–472.
TACAS-2003-Schmidt #invariant #petri net #using
Using Petri Net Invariants in State Space Construction (KS0), pp. 473–488.
TACAS-2003-StollerC #reduction
Optimistic Synchronization-Based State-Space Reduction (SDS, EC), pp. 489–504.
TACAS-2003-VaziriJ #constraints #theorem proving
Checking Properties of Heap-Manipulating Procedures with a Constraint Solver (MV, DJ), pp. 505–520.
TACAS-2003-BerezinGD #linear #online
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic (SB, VG, DLD), pp. 521–536.
TACAS-2003-ConchonK
Strategies for Combining Decision Procedures (SC, SK), pp. 537–552.
TACAS-2003-KhurshidPV #execution #model checking #symbolic computation #testing
Generalized Symbolic Execution for Model Checking and Testing (SK, CSP, WV), pp. 553–568.
TACAS-2003-BarayCDM #functional #generative #testing #validation
Code-Based Test Generation for Validation of Functional Processor Descriptions (FB, PC, DD, HM), pp. 569–584.
TACAS-2003-GrooteH #scalability #visualisation
Large State Space Visualization (JFG, FvH), pp. 585–590.
TACAS-2003-BigotFGLLPR #automation #generative #testing
Automatic Test Generation with AGATHA (CB, AF, JPG, AL, DL, JYP, NR), pp. 591–596.
TACAS-2003-UchitelCKM #behaviour #named #tool support #using
LTSA-MSC: Tool Support for Behaviour Model Elaboration Using Implied Scenarios (SU, RC, JK, JM), pp. 597–601.

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.