Holger Hermanns, Jens Palsberg
Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS, 2006.

@proceedings{TACAS-2006,
	address       = "Vienna, Austria",
	doi           = "10.1007/11691372",
	editor        = "Holger Hermanns and Jens Palsberg",
	isbn          = "3-540-33056-9",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}",
	volume        = 3920,
	year          = 2006,
}

Contents (35 items)

7 ×#verification
5 ×#refinement
4 ×#abstraction
4 ×#logic
4 ×#model checking
4 ×#named
4 ×#source code
3 ×#automation
3 ×#concurrent
3 ×#performance

TACAS-2006-JhaSWR #automaton #trust

Weighted Pushdown Systems and Trust-Management Systems (SJ, SS, HW, TWR), pp. 1–26.

TACAS-2006-DeshmukhEG #automation #data type #verification

Automatic Verification of Parameterized Data Structures (JVD, EAE, PG), pp. 27–41.

TACAS-2006-YangBR #verification #π-calculus

Parameterized Verification of π-Calculus Systems (PY, SB, CRR), pp. 42–57.

TACAS-2006-BrownP #protocol #verification

Easy Parameterized Verification of Biphase Mark and 8N1 Protocols (GMB, LP), pp. 58–72.

TACAS-2006-DwyerHHRRW #concurrent #effectiveness #object-oriented #reduction #slicing #source code

Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented Programs (MBD, JH, MH, VPR, R, TW), pp. 73–89.

TACAS-2006-SiminiceanuC #diagrams #metric

New Metrics for Static Variable Ordering in Decision Diagrams (RS, GC), pp. 90–104.

TACAS-2006-KettleKS

Widening ROBDDs with Prime Implicants (NK, AK, TS), pp. 105–119.

TACAS-2006-ThomasCP #performance #reachability #using

Efficient Guided Symbolic Reachability Using Reachability Expressions (DT, SC, PKP), pp. 120–134.

TACAS-2006-GanaiTG #encoding #integration #lazy evaluation #logic #named

SDSAT: Tight Integration of Small Domain Encoding and Lazy Approaches in a Separation Logic Solver (MKG, MT, AG), pp. 135–150.

TACAS-2006-Chaki #certification #satisfiability

SAT-Based Software Certification (SC), pp. 151–166.

TACAS-2006-FontaineMMNT #automation #interactive #proving #smt #towards

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants (PF, JYM, SM, LPN, AFT), pp. 167–181.

TACAS-2006-CollavizzaR #constraints #programming #verification

Exploration of the Capabilities of Constraint Programming for Software Verification (HC, MR), pp. 182–196.

TACAS-2006-KonigK #abstraction #analysis #graph transformation #refinement

Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems (BK, VK), pp. 197–211.

TACAS-2006-GurfinkelC #abstraction #question #why

Why Waste a Perfectly Good Abstraction? (AG, MC), pp. 212–226.

TACAS-2006-LiS #abstraction #bound #model checking #performance #refinement

Efficient Abstraction Refinement in Interpolation-Based Unbounded Model Checking (BL, FS), pp. 227–241.

TACAS-2006-KroeningS #approximate #image #logic

Approximating Predicate Images for Bit-Vector Logic (DK, NS), pp. 242–256.

TACAS-2006-ChatterjeeH #game studies

Finitary Winning in ω-Regular Games (KC, TAH), pp. 257–271.

TACAS-2006-NiebertP #ltl #model checking #partial order #performance

Efficient Model Checking for LTL with Partial Order Snapshots (PN, DP), pp. 272–286.

TACAS-2006-DistefanoOY #analysis #logic

A Local Shape Analysis Based on Separation Logic (DD, PWO, HY), pp. 287–302.

TACAS-2006-GhicaM #composition #concurrent #higher-order #source code

Compositional Model Extraction for Higher-Order Concurrent Programs (DRG, ASM), pp. 303–317.

TACAS-2006-LeueW #approach #graph #proving #termination

A Region Graph Based Approach to Termination Proofs (SL, WW), pp. 318–333.

TACAS-2006-ChakiCKRT #c #concurrent #message passing #recursion #source code #verification

Verifying Concurrent Message-Passing C Programs with Recursive Calls (SC, EMC, NK, TWR, TT), pp. 334–349.

TACAS-2006-HabermehlIV #source code #verification

Automata-Based Verification of Programs with Tree Updates (PH, RI, TV), pp. 350–364.

TACAS-2006-GuptaJ #comparison #control flow #effectiveness #fault #testing

An Experimental Comparison of the Effectiveness of Control Flow Based Testing Approaches on Seeded Faults (AG, PJ), pp. 365–378.

TACAS-2006-GroceJ #program analysis

Exploiting Traces in Program Analysis (AG, RJ), pp. 379–393.

TACAS-2006-SenVA #markov #model checking #nondeterminism

Model-Checking Markov Chains in the Presence of Uncertainties (KS, MV, GA), pp. 394–410.

TACAS-2006-OuaknineW #decidability #logic #metric #safety

Safety Metric Temporal Logic Is Fully Decidable (JO, JW), pp. 411–425.

TACAS-2006-SokolskyKL #graph #similarity

Simulation-Based Graph Similarity (OS, SK, IL), pp. 426–440.

TACAS-2006-HintonKNP #automation #named #probability #verification

PRISM: A Tool for Automatic Verification of Probabilistic Systems (AH, MZK, GN, DP), pp. 441–444.

TACAS-2006-GaravelMBCDJSS #distributed #generative #tool support

DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation (HG, RM, DB, AC, ND, CJ, ISS, GS), pp. 445–449.

TACAS-2006-LomuscioR #model checking #multi #named

MCMAS: A Model Checker for Multi-agent Systems (AL, FR), pp. 450–454.

TACAS-2006-BolligKSS #named #specification

MSCan — A Tool for Analyzing MSC Specifications (BB, CK, MS, VS), pp. 455–458.

TACAS-2006-JhalaM #approach #refinement

A Practical and Complete Approach to Predicate Refinement (RJ, KLM), pp. 459–473.

TACAS-2006-GulavaniR #abstract interpretation #refinement

Counterexample Driven Refinement for Abstract Interpretation (BSG, SKR), pp. 474–488.

TACAS-2006-EsparzaKS #abstraction #automaton #refinement

Abstraction Refinement with Craig Interpolation and Symbolic Pushdown Systems (JE, SK, SS), pp. 489–503.