Proceedings of the 11th 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

Nicolas Halbwachs, Lenore D. Zuck
Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS, 2005.

TCS
DBLP
Scholar
DOI
Full names Links ISxN
@proceedings{TACAS-2005,
	address       = "Edinburgh, Scotland, United Kingdom",
	doi           = "10.1007/b107194",
	editor        = "Nicolas Halbwachs and Lenore D. Zuck",
	isbn          = "3-540-25333-5",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}",
	volume        = 3440,
	year          = 2005,
}

Contents (42 items)

TACAS-2005-McMillan #model checking
Applications of Craig Interpolants in Model Checking (KLM), pp. 1–12.
TACAS-2005-BouajjaniHMV #model checking #source code #verification
Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking (AB, PH, PM, TV), pp. 13–29.
TACAS-2005-AbdullaLdR #transducer
Simulation-Based Iteration of Tree Transducers (PAA, AL, Jd, AR), pp. 30–44.
TACAS-2005-VardhanSVA #using #verification
Using Language Inference to Verify ω-Regular Properties (AV, KS, MV, GA), pp. 45–60.
TACAS-2005-AlurCEM #detection #on the fly #reachability #recursion #state machine
On-the-Fly Reachability and Cycle Detection for Recursive State Machines (RA, SC, KE, PM), pp. 61–76.
TACAS-2005-BinghamH #empirical #infinity #performance #verification
Empirically Efficient Verification for a Class of Infinite-State Systems (JDB, AJH), pp. 77–92.
TACAS-2005-QadeerR #bound #concurrent #model checking
Context-Bounded Model Checking of Concurrent Software (SQ, JR), pp. 93–107.
TACAS-2005-IsobeR #csp #proving #refinement #theorem proving
A Generic Theorem Prover of CSP Refinement (YI, MR), pp. 108–123.
TACAS-2005-PnueliPR #analysis
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems (AP, AP, AR), pp. 124–139.
TACAS-2005-RanzatoT #abstract interpretation #algorithm #refinement
An Abstract Interpretation-Based Refinement Algorithm for Strong Preservation (FR, FT), pp. 140–156.
TACAS-2005-KomondoorRCF #comprehension #dependent type
Dependent Types for Program Understanding (RK, GR, SC, JF), pp. 157–173.
TACAS-2005-SchwoonE #algorithm #on the fly #verification
A Note on On-the-Fly Verification Algorithms (SS, JE), pp. 174–190.
TACAS-2005-HammerKM #ltl #model checking #on the fly
Truly On-the-Fly LTL Model Checking (MH, AK, SM), pp. 191–205.
TACAS-2005-KupfermanV #automaton #infinity #nondeterminism #word
Complementation Constructions for Nondeterministic Automata on Infinite Words (OK, MYV), pp. 206–221.
TACAS-2005-Marrero #using
Using BDDs to Decide CTL (WM), pp. 222–236.
TACAS-2005-RemkeHC #infinity #markov #model checking
Model Checking Infinite-State Markov Chains (AR, BRH, LC), pp. 237–252.
TACAS-2005-EtessamiY #algorithm #probability #recursion #state machine #verification
Algorithmic Verification of Recursive Probabilistic State Machines (KE, MY), pp. 253–270.
TACAS-2005-GrosuS #model checking #monte carlo
Monte Carlo Model Checking (RG, SAS), pp. 271–286.
TACAS-2005-JinHS #analysis #performance
Efficient Conflict Analysis for Finding All Satisfying Assignments of a Boolean Circuit (HJ, HH, FS), pp. 287–300.
TACAS-2005-SharmaPC #bound #logic
Bounded Validity Checking of Interval Duration Logic (BS, PKP, SC), pp. 301–316.
TACAS-2005-BozzanoBCJRSS #incremental #linear #logic #satisfiability
An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic (MB, RB, AC, TAJ, PvR, SS, RS), pp. 317–333.
TACAS-2005-LeinoMO #proving #quantifier #theorem proving
A Two-Tier Technique for Supporting Quantifiers in a Lazily Proof-Explicating Theorem Prover (KRML, MM, XO), pp. 334–348.
TACAS-2005-JeannetJRZ #analysis #approximate #testing
Symbolic Test Selection Based on Approximate Analysis (BJ, TJ, VR, EZ), pp. 349–364.
TACAS-2005-XieMSN #execution #framework #generative #named #object-oriented #symbolic computation #testing #using
Symstra: A Framework for Generating Object-Oriented Unit Tests Using Symbolic Execution (TX, DM, WS, DN), pp. 365–381.
TACAS-2005-EmersonW #reduction #symmetry
Dynamic Symmetry Reduction (EAE, TW), pp. 382–396.
TACAS-2005-JainIGG #abstraction #locality
Localization and Register Sharing for Predicate Abstraction (HJ, FI, AG, MKG), pp. 397–412.
TACAS-2005-Jiang #invariant #on the
On Some Transformation Invariants Under Retiming and Resynthesis (JHRJ), pp. 413–428.
TACAS-2005-Genest #composition #sequence chart
Compositional Message Sequence Charts (CMSCs) Are Better to Implement Than MSCs (BG), pp. 429–444.
TACAS-2005-KuglerHPLB #logic #specification
Temporal Logic for Scenario-Based Specifications (HK, DH, AP, YL, YB), pp. 445–460.
TACAS-2005-WeimerN #detection #fault #mining #specification
Mining Temporal Specifications for Error Detection (WW, GCN), pp. 461–476.
TACAS-2005-HardingRS #algorithm #game studies #ltl #synthesis
A New Algorithm for Strategy Synthesis in LTL Games (AH, MR, PYS), pp. 477–492.
TACAS-2005-SchuppanB #ltl #model checking
Shortest Counterexamples for Symbolic Model Checking of LTL with Past (VS, AB), pp. 493–509.
TACAS-2005-GenestKMP #verification
Snapshot Verification (BG, DK, AM, DP), pp. 510–525.
TACAS-2005-BaoJ #model checking
Time-Efficient Model Checking with Magnetic Disk (TB, MDJ), pp. 526–540.
TACAS-2005-SuwimonteerabuthSE #bytecode #java #named
jMoped: A Java Bytecode Checker Based on Moped (DS, SS, JE), pp. 541–545.
TACAS-2005-ChenR #java #monitoring #named #programming
Java-MOP: A Monitoring Oriented Programming Environment for Java (FC, GR), pp. 546–550.
TACAS-2005-BouquetDLU #ml #named #specification #using
JML-Testing-Tools: A Symbolic Animator for JML Specifications Using CLP (FB, FD, BL, MU), pp. 551–556.
TACAS-2005-MargariaNS #integration #named #tool support
jETI: A Tool for Remote Tool Integration (TMS, RN, BS), pp. 557–562.
TACAS-2005-KellerSBS #c #debugging #model checking #named #source code
FocusCheck: A Tool for Model Checking and Debugging Sequential C Programs (CWK, DS, SB, SAS), pp. 563–569.
TACAS-2005-ClarkeKSY #abstraction #named #satisfiability
SATABS: SAT-Based Predicate Abstraction for ANSI-C (EMC, DK, NS, KY), pp. 570–574.
TACAS-2005-GanaiGA #framework #model checking #named #platform #satisfiability #scalability #verification
DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems (MKG, AG, PA), pp. 575–580.
TACAS-2005-BergaminiDJM #bisimulation #composition #equivalence #named #on the fly
BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking (DB, ND, CJ, RM), pp. 581–585.

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.