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

@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)

10 ×#model checking
9 ×#named
7 ×#verification
4 ×#algorithm
4 ×#on the fly
4 ×#using
3 ×#analysis
3 ×#infinity
3 ×#logic
3 ×#ltl

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.