Christel Baier, Cesare Tinelli
Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS, 2015.

@proceedings{TACAS-2015,
	address       = "London, England, United Kingdom",
	doi           = "10.1007/978-3-662-46681-0",
	editor        = "Christel Baier and Cesare Tinelli",
	isbn          = "978-3-662-46680-3",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems}",
	volume        = 9035,
	year          = 2015,
}

Contents (62 items)

20 ×#named
15 ×#contest
11 ×#verification
10 ×#source code
9 ×#analysis
8 ×#model checking
5 ×#synthesis
4 ×#automaton
4 ×#framework
4 ×#memory management

TACAS-2015-GuanTAS0 #analysis #refinement #scalability

Scalable Timing Analysis with Refinement (NG, YT, JA, MS, WY), pp. 3–18.

TACAS-2015-JeanninGKGSZP #hybrid

A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System (JBJ, KG, YK, RG, AS, EZ, AP), pp. 21–36.

TACAS-2015-Immler #analysis #reachability

Verified Reachability Analysis of Continuous Systems (FI), pp. 37–51.

TACAS-2015-CimattiGMT #hybrid #model checking #named #smt

HyComp: An SMT-Based Model Checker for Hybrid Systems (AC, AG, SM, ST), pp. 52–67.

TACAS-2015-DuggiralaMVP #modelling #named #verification

C2E2: A Verification Tool for Stateflow Models (PSD, SM, MV, MP), pp. 68–82.

TACAS-2015-AlbertFR #analysis #cumulative

Non-cumulative Resource Analysis (EA, JCF, GRD), pp. 85–100.

TACAS-2015-KumarSK #concept #scalability #slicing

Value Slice: A New Slicing Concept for Scalable Property Checking (SK, AS, UPK), pp. 101–115.

TACAS-2015-ZengSLH #precise #predict

A Method for Improving the Precision and Coverage of Atomicity Violation Predictions (RZ, ZS, SL, XH), pp. 116–130.

TACAS-2015-ChenHSW #commutative #reduction

Commutativity of Reducers (YFC, CDH, NS, BYW), pp. 131–146.

TACAS-2015-UnnoT #horn clause #recursion

Inferring Simple Solutions to Recursion-Free Horn Clauses via Sampling (HU, TT), pp. 149–163.

TACAS-2015-NamjoshiT #analysis #network #process

Analysis of Dynamic Process Networks (KSN, RJT), pp. 164–178.

TACAS-2015-BrazdilCFK #multi #named #synthesis

MultiGain: A Controller Synthesis Tool for MDPs with Multiple Mean-Payoff Objectives (TB, KC, VF, AK), pp. 181–187.

TACAS-2015-DemasiCRMA #fault tolerance #named #source code #specification

syntMaskFT: A Tool for Synthesizing Masking Fault-Tolerant Programs from Deontic Specifications (RD, PFC, NR, TSEM, NA), pp. 188–193.

TACAS-2015-BjornerPF #named #optimisation #smt

νZ — An Optimizing SMT Solver (NB, ADP, LF), pp. 194–199.

TACAS-2015-KongGCC #analysis #hybrid #named

dReach: δ-Reachability Analysis for Hybrid Systems (SK, SG, WC, EMC), pp. 200–205.

TACAS-2015-DavidJLMT #stratego

Uppaal Stratego (AD, PGJ, KGL, MM, JHT), pp. 206–211.

TACAS-2015-DjoudiB #analysis #low level #named

BINSEC: Binary Code Analysis with Low-Level Regions (AD, SB), pp. 212–217.

TACAS-2015-FleuryLPV #analysis #framework #named

Insight: An Open Binary Analysis Framework (EF, OL, GP, AV), pp. 218–224.

TACAS-2015-ArmandoBCCMMM #framework #mobile #named #platform #security #static analysis #verification

SAM: The Static Analysis Module of the MAVERIC Mobile App Security Verification Platform (AA, GB, GC, GC, GDM, RM, AM), pp. 225–230.

TACAS-2015-Thierry-Mieg #model checking #using

Symbolic Model-Checking Using ITS-Tools (YTM), pp. 231–237.

TACAS-2015-HansenWCNK #model checking #semantics #statistics

Semantic Importance Sampling for Statistical Model Checking (JPH, LW, SC, DdN, MHK), pp. 241–255.

TACAS-2015-BassetKTW #game studies #multi #probability #synthesis

Strategy Synthesis for Stochastic Games with Multiple Long-Run Objectives (NB, MZK, UT, CW), pp. 256–271.

TACAS-2015-SoudjaniGA #abstraction #probability #process

FAUST 2 : Formal Abstractions of Uncountable-STate STochastic Processes (SEZS, CG, AA), pp. 272–286.

TACAS-2015-BransenBCD #attribute grammar #order #scheduling #using

Linearly Ordered Attribute Grammar Scheduling Using SAT-Solving (JB, LTvB, KC, AD), pp. 289–303.

TACAS-2015-ChakrabortyFMSV #generative #on the #parallel #satisfiability #scalability

On Parallel Scalable Uniform SAT Witness Generation (SC, DJF, KSM, SAS, MYV), pp. 304–319.

TACAS-2015-ChistikovDM #approximate #estimation #probability #smt #source code

Approximate Counting in SMT and Value Estimation for Probabilistic Programs (DVC, RD, RM), pp. 320–334.

TACAS-2015-SebastianiT #cost analysis #modulo theories #optimisation

Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions (RS, PT), pp. 335–349.

TACAS-2015-AbdullaAAJLS #model checking

Stateless Model Checking for TSO and PSO (PAA, SA, MFA, BJ, CL, KFS), pp. 353–367.

TACAS-2015-Wijs #branch #gpu #similarity

GPU Accelerated Strong and Branching Bisimilarity Checking (AW), pp. 368–383.

TACAS-2015-CookKP #infinity

Fairness for Infinite-State Systems (BC, HK, NP), pp. 384–398.

TACAS-2015-Beyer #verification

Software Verification and Verifiable Witnesses — (Report on SV-COMP 2015) (DB), pp. 401–416.

TACAS-2015-StroderAFHG #c #contest #memory management #named #safety #source code #termination

AProVE: Termination and Memory Safety of C Programs — (Competition Contribution) (TS, CA, FF, JH, JG), pp. 417–419.

TACAS-2015-WangB #contest #named

Cascade — (Competition Contribution) (WW, CB), pp. 420–422.

TACAS-2015-DanglLW #contest #float #recursion #source code

CPAchecker with Support for Recursive Programs and Floating-Point Arithmetic — (Competition Contribution) (MD, SL, PW), pp. 423–425.

TACAS-2015-ChenHTWW #contest #named #program transformation #recursion #source code #text-to-text #verification

CPArec: Verifying Recursive Programs via Source-to-Source Program Transformation — (Competition Contribution) (YFC, CH, MHT, BYW, FW), pp. 426–428.

TACAS-2015-AledoE #contest #embedded #framework #verification

FramewORk for Embedded System verification — (Competition Contribution) (PGdA, PSE), pp. 429–431.

TACAS-2015-HolikHLRSV #analysis #automaton #contest #named #using

Forester: Shape Analysis Using Tree Automata — (Competition Contribution) (LH, MH, OL, AR, JS, TV), pp. 432–435.

TACAS-2015-TomascoI0TP #contest #memory management

MU-CSeq 0.3: Sequentialization by Read-Implicit and Coarse-Grained Memory Unwindings — (Competition Contribution) (ET, OI, BF, SLT, GP), pp. 436–438.

TACAS-2015-CassezMPS #composition #contest #named #refinement

Perentie: Modular Trace Refinement and Selective Value Tracking — (Competition Contribution) (FC, TM, EP, NS), pp. 439–442.

TACAS-2015-MullerPV #contest

Predator Hunting Party (Competition Contribution) (PM, PP, TV), pp. 443–446.

TACAS-2015-GurfinkelKN #c #contest #framework #named #source code #verification

SeaHorn: A Framework for Verifying C Programs (Competition Contribution) (AG, TK, JAN), pp. 447–450.

TACAS-2015-HaranCELQR #composition #contest #verification

SMACK+Corral: A Modular Verifier — (Competition Contribution) (AH, MC, ME, AL, SQ, ZR), pp. 451–454.

TACAS-2015-HeizmannDLMP #array #contest

Ultimate Automizer with Array Interpolation — (Competition Contribution) (MH, DD, JL, BM, AP), pp. 455–457.

TACAS-2015-NutzDMP #contest #memory management #safety

ULTIMATE KOJAK with Memory Safety Checks — (Competition Contribution) (AN, DD, MMM, AP), pp. 458–460.

TACAS-2015-Nguyen0TP #bound #c #contest #lazy evaluation #source code

Unbounded Lazy-CSeq: A Lazy Sequentialization Tool for C Programs with Unbounded Context Switches — (Competition Contribution) (TLN, BF, SLT, GP), pp. 461–463.

TACAS-2015-Urban #abstract domain #contest #named #termination

FuncTion: An Abstract Domain Functor for Termination — (Competition Contribution) (CU), pp. 464–466.

TACAS-2015-GiacobbeGGHPP #model checking #network

Model Checking Gene Regulatory Networks (MG, CCG, AG, TAH, TP, TP), pp. 469–483.

TACAS-2015-Sankur #analysis #automaton #robust

Symbolic Quantitative Robustness Analysis of Timed Automata (OS), pp. 484–498.

TACAS-2015-AlurMT #refinement #specification #synthesis

Pattern-Based Refinement of Assume-Guarantee Specifications in Reactive Synthesis (RA, SM, UT), pp. 501–516.

TACAS-2015-BloemCJK #concurrent #source code #synthesis

Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information (RB, KC, SJ, RK), pp. 517–532.

TACAS-2015-BloemKKW #runtime #synthesis

Shield Synthesis: — Runtime Enforcement for Reactive Systems (RB, BK, RK, CW), pp. 533–548.

TACAS-2015-TomascoI0TP15a #concurrent #memory management #source code #verification

Verifying Concurrent Programs by Memory Unwinding (ET, OI, BF, SLT, GP), pp. 551–565.

TACAS-2015-TschannenFNP #functional #named #object-oriented #source code #verification

AutoProof: Auto-Active Functional Verification of Object-Oriented Programs (JT, CAF, MN, NP), pp. 566–580.

TACAS-2015-CiniF #ltl #proving #runtime #verification

An LTL Proof System for Runtime Verification (CC, AF), pp. 581–595.

TACAS-2015-RegerCR #monitoring #named #runtime

MarQ: Monitoring at Runtime with QEA (GR, HCC, DER), pp. 596–610.

TACAS-2015-RenaultDKP #automaton #model checking #parallel

Parallel Explicit Model Checking for Generalized Büchi Automata (ER, ADL, FK, DP), pp. 613–627.

TACAS-2015-KiniV #automaton #ltl #probability

Limit Deterministic and Probabilistic Automata for LTL ∖ GU (DK, MV), pp. 628–642.

TACAS-2015-MolnarDVB #incremental #induction #ltl #model checking #proving

Saturation-Based Incremental LTL Model Checking with Inductive Proofs (VM, DD, AV, TB), pp. 643–657.

TACAS-2015-FiedorHLV #anti

Nested Antichains for WS1S (TF, LH, OL, TV), pp. 658–674.

TACAS-2015-DijkP #diagrams #manycore #named

Sylvan: Multi-Core Decision Diagrams (TvD, JvdP), pp. 677–691.

TACAS-2015-KantLMPBD #independence #model checking #named

LTSmin: High-Performance Language-Independent Model Checking (GK, AL, JM, JvdP, SB, TvD), pp. 692–707.

TACAS-2015-KriouileS #formal method #using #verification

Using a Formal Model to Improve Verification of a Cache-Coherent System-on-Chip (AK, WS), pp. 708–722.