Kurt Jensen, Andreas Podelski
Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS, 2004.
@proceedings{TACAS-2004, address = "Barcelona, Spain", editor = "Kurt Jensen and Andreas Podelski", isbn = "3-540-21299-X", publisher = "{Springer International Publishing}", series = "{Lecture Notes in Computer Science}", title = "{Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}", volume = 2988, year = 2004, }
Contents (43 items)
- TACAS-2004-LahiriBGT #similarity
- Revisiting Positive Equality (SKL, REB, AG, MT), pp. 1–15.
- TACAS-2004-McMillan #proving #theorem proving
- An Interpolating Theorem Prover (KLM), pp. 16–30.
- TACAS-2004-RaviS #bound #model checking
- Minimal Assignments for Bounded Model Checking (KR, FS), pp. 31–45.
- TACAS-2004-YounesKNP #empirical #model checking #probability #statistics
- Numerical vs. Statistical Probabilistic Model Checking: An Empirical Study (HLSY, MZK, GN, DP), pp. 46–60.
- TACAS-2004-BaierHHK #bound #markov #performance #process #reachability
- Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision Processes (CB, BRH, HH, JPK), pp. 61–76.
- TACAS-2004-AlfaroFHMS #model checking
- Model Checking Discounted Temporal Properties (LdA, MF, TAH, RM, MS), pp. 77–92.
- TACAS-2004-BallLX #automation #modelling
- Automatic Creation of Environment Models via Training (TB, VL, FX), pp. 93–107.
- TACAS-2004-Groce #distance #fault #metric
- Error Explanation with Distance Metrics (AG), pp. 108–122.
- TACAS-2004-SenRA #analysis #online #parallel #performance #predict #safety #source code #thread
- Online Efficient Predictive Safety Analysis of Multithreaded Programs (KS, GR, GA), pp. 123–138.
- TACAS-2004-DiethersH #design #named #object-oriented #using #verification
- Vooduu: Verification of Object-Oriented Designs Using UPPAAL (KD, MH), pp. 139–143.
- TACAS-2004-PiazzaPR #named #persistent #security
- CoPS — Checker of Persistent Security (CP, EP, SR), pp. 144–152.
- TACAS-2004-VirtanenHVNE #verification
- Tampere Verification Tool (HV, HH, AV, JN, TE), pp. 153–157.
- TACAS-2004-DengDHM #aspect-oriented #framework #named
- SyncGen: An Aspect-Oriented Framework for Synchronization (XD, MBD, JH, MM), pp. 158–162.
- TACAS-2004-Muller-OlmY #animation #game studies #model checking #named
- MetaGame: An Animation Tool for Model-Checking Games (MMO, HY), pp. 163–167.
- TACAS-2004-ClarkeKL #source code
- A Tool for Checking ANSI-C Programs (EMC, DK, FL), pp. 168–176.
- TACAS-2004-MailundW #graph #reachability #using
- Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line Method (TM, MW), pp. 177–191.
- TACAS-2004-Schmidt #automation #generative
- Automated Generation of a Progress Measure for the Sweep-Line Method (KS0), pp. 192–204.
- TACAS-2004-GeldenhuysV #algorithm #ltl #on the fly #performance #verification
- Tarjan’s Algorithm Makes On-the-Fly LTL Verification More Efficient (JG, AV), pp. 205–219.
- TACAS-2004-RasmussenLS #automaton #scheduling #using
- Resource-Optimal Scheduling Using Priced Timed Automata (JIR, KGL, KS), pp. 220–235.
- TACAS-2004-KrcalY #analysis #automaton #decidability #problem #scheduling #using
- Decidable and Undecidable Problems in Schedulability Analysis Using Timed Automata (PK, WY), pp. 236–250.
- TACAS-2004-NielsonNSBHPS
- The Succinct Solver Suite (FN, HRN, HS, MB, RRH, HP, HS), pp. 251–265.
- TACAS-2004-LingerS #analysis #constraints #ml #theorem proving #type inference
- Binding-Time Analysis for MetaML via Type Inference and Constraint Solving (NL, TS), pp. 266–279.
- TACAS-2004-SuW #analysis #constraints
- A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and Narrowings (ZS, DW), pp. 280–295.
- TACAS-2004-LugiezNZ #approach #automaton #explosion #partial order #problem #semantics
- A Partial Order Semantics Approach to the Clock Explosion Problem of Timed Automata (DL, PN, SZ), pp. 296–311.
- TACAS-2004-BehrmannBLP #abstraction #automaton #bound
- Lower and Upper Bounds in Zone Based Abstractions of Timed Automata (GB, PB, KGL, RP), pp. 312–326.
- TACAS-2004-LeueMW #bound #modelling #scalability #uml
- A Scalable Incomplete Test for the Boundedness of UML RT Models (SL, RM, WW), pp. 327–341.
- TACAS-2004-DelzannoG #automation #encryption #protocol #verification
- Automatic Verification of Time Sensitive Cryptographic Protocols (GD, PG), pp. 342–356.
- TACAS-2004-LindseyP #verification
- Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinder (AEL, CP), pp. 357–371.
- TACAS-2004-BeauquierCP #automation #first-order #logic #parametricity #protocol #state machine #verification
- Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic (DB, TC, EP), pp. 372–387.
- TACAS-2004-BallCDR #abstraction #approximate
- Refining Approximations in Software Predicate Abstraction (TB, BC, SD, SKR), pp. 388–403.
- TACAS-2004-RobbyRDH #framework #model checking #specification #using
- Checking Strong Specifications Using an Extensible Software Model Checking Framework (R, ER, MBD, JH), pp. 404–420.
- TACAS-2004-AbramskyGMO #composition #game studies #modelling #semantics #verification
- Applying Game Semantics to Compositional Software Modeling and Verification (SA, DRG, ASM, CHLO), pp. 421–435.
- TACAS-2004-GrooteK #equation #fixpoint
- Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed Points (JFG, MK), pp. 436–450.
- TACAS-2004-GurfinkelC #how #question
- How Vacuous Is Vacuous? (AG, MC), pp. 451–466.
- TACAS-2004-AlurEM #logic
- A Temporal Logic of Nested Calls and Returns (RA, KE, PM), pp. 467–481.
- TACAS-2004-FangPPZ #liveness #ranking
- Liveness with Incomprehensible Ranking (YF, NP, AP, LDZ), pp. 482–496.
- TACAS-2004-QianN #abstraction #database #invariant #model checking
- Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern Databases (KQ, AN), pp. 497–511.
- TACAS-2004-GopanDDRS
- Numeric Domains with Summarized Dimensions (DG, FD, ND, TWR, SS), pp. 512–529.
- TACAS-2004-YorshRS #analysis
- Symbolically Computing Most-Precise Abstract Operations for Shape Analysis (GY, TWR, SS), pp. 530–545.
- TACAS-2004-ShohamG #abstraction
- Monotonic Abstraction-Refinement for CTL (SS, OG), pp. 546–560.
- TACAS-2004-BoigelotLW #model checking
- ω-Regular Model Checking (BB, AL, PW), pp. 561–575.
- TACAS-2004-BardinFL #automaton #performance
- FASTer Acceleration of Counter Automata in Practice (SB, AF, JL), pp. 576–590.
- TACAS-2004-KupfermanV #certification
- From Complementation to Certification (OK, MYV), pp. 591–606.
7 ×#model checking
7 ×#verification
5 ×#analysis
5 ×#automaton
5 ×#using
4 ×#abstraction
4 ×#automation
4 ×#bound
4 ×#named
4 ×#performance
7 ×#verification
5 ×#analysis
5 ×#automaton
5 ×#using
4 ×#abstraction
4 ×#automation
4 ×#bound
4 ×#named
4 ×#performance