zbMATH — the first resource for mathematics

Tools and algorithms for the construction and analysis of systems. 19th international conference, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16–24, 2013. Proceedings. (English) Zbl 1268.68030
Lecture Notes in Computer Science 7795. Berlin: Springer (ISBN 978-3-642-36741-0/pbk). xxiv, 646 p. (2013).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. For the preceding conference see [Zbl 1238.68014].
Indexed articles:
Bacci, Giorgio; Bacci, Giovanni; Larsen, Kim G.; Mardare, Radu, On-the-fly exact computation of bisimilarity distances, 1-15 [Zbl 1381.68218]
Eisentraut, Christian; Hermanns, Holger; Schuster, Johann; Turrini, Andrea; Zhang, Lijun, The quest for minimal quotients for probabilistic automata, 16-31 [Zbl 1381.68115]
Benedikt, Michael; Lenhardt, Rastislav; Worrell, James, LTL model checking of interval Markov chains, 32-46 [Zbl 1381.68147]
Cook, Byron; See, Abigail; Zuleger, Florian, Ramsey versus lexicographic termination proving, 47-61 [Zbl 1381.68050]
Bansal, Kshitij; Koskinen, Eric; Wies, Thomas; Zufferey, Damien, Structural counter abstraction, 62-77 [Zbl 1381.68194]
John, Ajith K.; Chakraborty, Supratik, Extending quantifier elimination to linear inequalities on bit-vectors, 78-92 [Zbl 1381.68055]
Cimatti, Alessandro; Griggio, Alberto; Schaafsma, Bastiaan Joost; Sebastiani, Roberto, The MathSAT5 SMT solver, 93-107 [Zbl 1381.68153]
Belov, Anton; Järvisalo, Matti; Marques-Silva, Joao, Formula preprocessing in MUS extraction, 108-123 [Zbl 1381.68146]
Christ, Jürgen; Hoenicke, Jochen; Nutz, Alexander, Proof tree preserving interpolation, 124-138 [Zbl 1381.68152]
Wieringa, Siert; Heljanko, Keijo, Asynchronous multi-core incremental SAT solving, 139-153 [Zbl 1381.68186]
Huang, Chung-Hao; Schewe, Sven; Wang, Farn, Model-checking iterated games, 154-168 [Zbl 1381.68167]
Bohy, Aaron; Bruyère, Véronique; Filiot, Emmanuel; Raskin, Jean-François, Synthesis from LTL specifications with mean-payoff objectives, 169-184 [Zbl 1381.68149]
Chen, Taolue; Forejt, Vojtěch; Kwiatkowska, Marta; Parker, David; Simaitis, Aistis, PRISM-games: a model checker for stochastic multi-player games, 185-191 [Zbl 1381.68151]
Mateescu, Radu; Salaün, Gwen, PIC2LNT: model transformation for model checking an applied pi-calculus, 192-198 [Zbl 1381.68175]
Cranen, Sjoerd; Groote, Jan Friso; Keiren, Jeroen J. A.; Stappers, Frank P. M.; de Vink, Erik P.; Wesselink, Wieger; Willemse, Tim A. C., An overview of the mCRL2 toolset and its recent advances, 199-213 [Zbl 1381.68198]
Godefroid, Patrice; Yannakakis, Mihalis, Analysis of Boolean programs, 214-229 [Zbl 1381.68164]
Minamide, Yasuhiko, Weighted pushdown systems with indexed weight domains, 230-244 [Zbl 1381.68176]
Ganty, Pierre; Iosif, Radu; Konečný, Filip, Underapproximation of procedure summaries for integer programs, 245-259 [Zbl 1381.68052]
Grigore, Radu; Distefano, Dino; Petersen, Rasmus Lerchedahl; Tzevelekos, Nikos, Runtime verification based on register automata, 260-276 [Zbl 1381.68165]
Gange, Graeme; Navas, Jorge A.; Stuckey, Peter J.; Søndergaard, Harald; Schachte, Peter, Unbounded model-checking with interpolation for regular language constraints, 277-291 [Zbl 1381.68162]
Fedyukovich, Grigory; Sery, Ondrej; Sharygina, Natasha, eVolCheck: incremental upgrade checker for C, 292-307 [Zbl 1381.68159]
Vizel, Yakir; Grumberg, Orna; Shoham, Sharon, Intertwined forward-backward reachability analysis using interpolants, 308-323 [Zbl 1381.68184]
Abdulla, Parosh Aziz; Haziza, Frédéric; Holík, Lukáš; Jonsson, Bengt; Rezine, Ahmed, An integrated specification and verification technique for highly concurrent data structures, 324-338 [Zbl 1381.68141]
Linden, Alexander; Wolper, Pierre, A verification-based approach to memory fence insertion in PSO memory systems, 339-353 [Zbl 1381.68173]
White, David H.; Lüttgen, Gerald, Identifying dynamic data structures by learning evolving patterns in memory, 354-369 [Zbl 1381.68064]
Li, Boyang; Dillig, Isil; Dillig, Thomas; McMillan, Ken; Sagiv, Mooly, Synthesis of circular compositional program proofs via abduction, 370-384 [Zbl 1381.68057]
Kempf, Jean-François; Bozga, Marius; Maler, Oded, As soon as probable: optimal scheduling under stochastic uncertainty, 385-400 [Zbl 1381.68022]
Jovanović, Aleksandra; Lime, Didier; Roux, Olivier H., Integer parameter synthesis for timed automata, 401-415 [Zbl 1381.68121]
Song, Fu; Touili, Tayssir, LTL model-checking for malware detection, 416-431 [Zbl 1381.68182]
Ferrara, Anna Lisa; Madhusudan, P.; Parlato, Gennaro, Policy analysis for self-administrated role-based access control, 432-447 [Zbl 1381.68025]
Koleini, Masoud; Ritter, Eike; Ryan, Mark, Model checking agent knowledge in dynamic access control policies, 448-462 [Zbl 1381.68171]
Nagy, Robert; Schneider, Gerardo; Timofeitchik, Aram, Automatic testing of real-time graphics systems, 463-477 [Zbl 1381.68177]
Ardeshir-Larijani, Ebrahim; Gay, Simon J.; Nagarajan, Rajagopal, Equivalence checking of quantum protocols, 478-492 [Zbl 1381.68144]
Blanchette, Jasmin Christian; Böhme, Sascha; Popescu, Andrei; Smallbone, Nicholas, Encoding monomorphic and polymorphic types, 493-507 [Zbl 1381.68259]
Bhat, Sooraj; Borgström, Johannes; Gordon, Andrew D.; Russo, Claudio, Deriving probability density functions from probabilistic functional programs, 508-522 [Zbl 1381.68030]
Gligoric, Milos; Majumdar, Rupak, Model checking database applications, 549-564 [Zbl 1381.68163]
Wijs, Anton; Engelen, Luc, Efficient property preservation checking of model refinements, 565-579 [Zbl 1381.68187]
Renault, Etienne; Duret-Lutz, Alexandre; Kordon, Fabrice; Poitrenaud, Denis, Strength-based decomposition of the property Büchi automaton for faster model checking, 580-593 [Zbl 1381.68133]

68-06 Proceedings, conferences, collections, etc. pertaining to computer science
68Q60 Specification and verification (program logics, model checking, etc.)
00B25 Proceedings of conferences of miscellaneous specific interest
Full Text: DOI