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

Nir Piterman, Scott A. Smolka
Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
TACAS, 2013.

TCS
DBLP
Scholar
DOI
Full names Links ISxN
@proceedings{TACAS-2013,
	address       = "Rome, Italy",
	doi           = "10.1007/978-3-642-36742-7",
	editor        = "Nir Piterman and Scott A. Smolka",
	isbn          = "978-3-642-36741-0",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems}",
	volume        = 7795,
	year          = 2013,
}

Contents (53 items)

TACAS-2013-BacciBLM #on the fly #similarity
On-the-Fly Exact Computation of Bisimilarity Distances (GB, GB, KGL, RM), pp. 1–15.
TACAS-2013-EisentrautHST0 #automaton #probability
The Quest for Minimal Quotients for Probabilistic Automata (CE, HH, JS, AT, LZ), pp. 16–31.
TACAS-2013-BenediktLW #ltl #markov #model checking
LTL Model Checking of Interval Markov Chains (MB, RL, JW), pp. 32–46.
TACAS-2013-CookSZ #proving #termination
Ramsey vs. Lexicographic Termination Proving (BC, AS, FZ), pp. 47–61.
TACAS-2013-BansalKWZ #abstraction
Structural Counter Abstraction (KB, EK, TW, DZ), pp. 62–77.
TACAS-2013-JohnC #linear #quantifier
Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors (AKJ, SC), pp. 78–92.
TACAS-2013-CimattiGSS #smt
The MathSAT5 SMT Solver (AC, AG, BJS, RS), pp. 93–107.
TACAS-2013-BelovJM #preprocessor
Formula Preprocessing in MUS Extraction (AB, MJ, JMS), pp. 108–123.
TACAS-2013-ChristHN #proving
Proof Tree Preserving Interpolation (JC, JH, AN), pp. 124–138.
TACAS-2013-WieringaH #incremental #manycore #satisfiability
Asynchronous Multi-core Incremental SAT Solving (SW, KH), pp. 139–153.
TACAS-2013-HuangSW #game studies #model checking
Model-Checking Iterated Games (CHH, SS, FW), pp. 154–168.
TACAS-2013-BohyBFR #ltl #specification #synthesis
Synthesis from LTL Specifications with Mean-Payoff Objectives (AB, VB, EF, JFR), pp. 169–184.
TACAS-2013-ChenFKPS #game studies #model checking #multi #named #probability
PRISM-games: A Model Checker for Stochastic Multi-Player Games (TC, VF, MZK, DP, AS), pp. 185–191.
TACAS-2013-MateescuS #model checking #model transformation #named #π-calculus
PIC2LNT: Model Transformation for Model Checking an Applied π-Calculus (RM, GS), pp. 192–198.
TACAS-2013-CranenGKSVWW #overview #tool support
An Overview of the mCRL2 Toolset and Its Recent Advances (SC, JFG, JJAK, FPMS, EPdV, WW, TACW), pp. 199–213.
TACAS-2013-GodefroidY #analysis #source code
Analysis of Boolean Programs (PG, MY), pp. 214–229.
TACAS-2013-Minamide #automaton
Weighted Pushdown Systems with Indexed Weight Domains (YM), pp. 230–244.
TACAS-2013-GantyIK #approximate #integer #source code #summary
Underapproximation of Procedure Summaries for Integer Programs (PG, RI, FK), pp. 245–259.
TACAS-2013-GrigoreDPT #automaton #runtime #verification
Runtime Verification Based on Register Automata (RG, DD, RLP, NT), pp. 260–276.
TACAS-2013-GangeNSSS #bound #constraints #model checking #regular expression
Unbounded Model-Checking with Interpolation for Regular Language Constraints (GG, JAN, PJS, HS, PS), pp. 277–291.
TACAS-2013-FedyukovichSS #c #incremental #named
eVolCheck: Incremental Upgrade Checker for C (GF, OS, NS), pp. 292–307.
TACAS-2013-VizelGS #analysis #reachability #using
Intertwined Forward-Backward Reachability Analysis Using Interpolants (YV, OG, SS), pp. 308–323.
TACAS-2013-AbdullaHHJR #concurrent #data type #specification #verification
An Integrated Specification and Verification Technique for Highly Concurrent Data Structures (PAA, FH, LH, BJ, AR), pp. 324–338.
TACAS-2013-LindenW #approach #memory management
A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems (AL, PW), pp. 339–353.
TACAS-2013-WhiteL #data type #evolution #identification #in memory #learning #memory management
Identifying Dynamic Data Structures by Learning Evolving Patterns in Memory (DHW, GL), pp. 354–369.
TACAS-2013-LiDDMS #abduction #composition #proving #synthesis
Synthesis of Circular Compositional Program Proofs via Abduction (BL, ID, TD, KLM, MS), pp. 370–384.
TACAS-2013-KempfBM #nondeterminism #probability #scheduling
As Soon as Probable: Optimal Scheduling under Stochastic Uncertainty (JFK, MB, OM), pp. 385–400.
TACAS-2013-JovanovicLR #automaton #integer #parametricity #synthesis
Integer Parameter Synthesis for Timed Automata (AJ, DL, OHR), pp. 401–415.
TACAS-2013-SongT #detection #ltl #model checking
LTL Model-Checking for Malware Detection (FS, TT), pp. 416–431.
TACAS-2013-FerraraMP #analysis #data access #policy #self
Policy Analysis for Self-administrated Role-Based Access Control (ALF, PM, GP), pp. 432–447.
TACAS-2013-KoleiniRR #data access #model checking #policy
Model Checking Agent Knowledge in Dynamic Access Control Policies (MK, ER, MR), pp. 448–462.
TACAS-2013-NagyST #automation #realtime #testing
Automatic Testing of Real-Time Graphics Systems (RN, GS, AT), pp. 463–477.
TACAS-2013-Ardeshir-LarijaniGN #equivalence #protocol #quantum
Equivalence Checking of Quantum Protocols (EAL, SJG, RN), pp. 478–492.
TACAS-2013-BlanchetteBPS #encoding #polymorphism
Encoding Monomorphic and Polymorphic Types (JCB, SB, AP, NS), pp. 493–507.
TACAS-2013-BhatBGR #functional #probability #source code
Deriving Probability Density Functions from Probabilistic Functional Programs (SB, JB, ADG, CVR), pp. 508–522.
TACAS-2013-BalasubramanianPKL #analysis #multi #named #statechart
Polyglot: Systematic Analysis for Multiple Statechart Formalisms (DB, CSP, GK, MRL), pp. 523–529.
TACAS-2013-AbdullaACLR #automation #precise
Memorax, a Precise and Sound Tool for Automatic Fence Insertion under TSO (PAA, MFA, YFC, CL, AR), pp. 530–536.
TACAS-2013-ChenW #algorithm #learning #library #named
BULL: A Library for Learning Algorithms of Boolean Functions (YFC, BYW), pp. 537–542.
TACAS-2013-BackesGHMS #android #named #requirements
AppGuard — Enforcing User Requirements on Android Apps (MB, SG, CH, MM, PvSR), pp. 543–548.
TACAS-2013-GligoricM #database #model checking
Model Checking Database Applications (MG, RM), pp. 549–564.
TACAS-2013-WijsE #performance
Efficient Property Preservation Checking of Model Refinements (AW, LE), pp. 565–579.
TACAS-2013-RenaultDKP #automaton #composition #model checking #performance
Strength-Based Decomposition of the Property Büchi Automaton for Faster Model Checking (ER, ADL, FK, DP), pp. 580–593.
TACAS-2013-Beyer #contest #summary #verification
Second Competition on Software Verification — (Summary of SV-COMP 2013) (DB0), pp. 594–609.
TACAS-2013-Lowe #analysis #contest
CPAchecker with Explicit-Value Analysis Based on CEGAR and Interpolation — (Competition Contribution) (SL), pp. 610–612.
TACAS-2013-Wendler #analysis #contest
CPAchecker with Sequential Combination of Explicit-State Analysis and Predicate Analysis — (Competition Contribution) (PW), pp. 613–615.
TACAS-2013-0002IP #c #contest #named
CSeq: A Sequentialization Tool for C — (Competition Contribution) (BF, OI, GP), pp. 616–618.
TACAS-2013-MorseCNF #bound #contest
Handling Unbounded Loops with ESBMC 1.20 — (Competition Contribution) (JM, LCC, DN, BF), pp. 619–622.
TACAS-2013-FalkeMS #bound #c #contest #model checking #named #source code #using
LLBMC: Improved Bounded Model Checking of C Programs Using LLVM — (Competition Contribution) (SF, FM, CS), pp. 623–626.
TACAS-2013-DudkaMPV #contest #low level #named #verification
Predator: A Tool for Verification of Low-Level List Manipulation — (Competition Contribution) (KD, PM, PP, TV), pp. 627–629.
TACAS-2013-SlabyST #contest #execution #named #slicing #symbolic computation
Symbiotic: Synergy of Instrumentation, Slicing, and Symbolic Execution — (Competition Contribution) (JS, JS, MT), pp. 630–632.
TACAS-2013-PopeeaR #concurrent #contest #multi #named #source code #thread #verification
Threader: A Verifier for Multi-threaded Programs — (Competition Contribution) (CP, AR), pp. 633–636.
TACAS-2013-AlbarghouthiGLCC #abstract interpretation #contest #named #verification
UFO: Verification with Interpolants and Abstract Interpretation — (Competition Contribution) (AA, AG, YL, SC, MC), pp. 637–640.
TACAS-2013-HeizmannCDEHLNSP #contest
Ultimate Automizer with SMTInterpol — (Competition Contribution) (MH, JC, DD, EE, JH, ML, AN, CS, AP), pp. 641–643.

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.