Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. (English) Zbl 1236.68007

Lecture Notes in Computer Science 7148. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). xi, 461 p. (2012).

Show indexed articles as search result.

The articles of this volume will be reviewed individually. For the preceding conference see Zbl 1206.68013.
Indexed articles:
Bouajjani, Ahmed; Drăgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela, Abstract domains for automated reasoning about list-manipulating programs with infinite data, 1-22 [Zbl 1325.68058]
Nipkow, Tobias, Teaching semantics with a proof assistant: no more LSD trip proofs, 24-38 [Zbl 1325.68005]
Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha, Whale: an interpolation-based algorithm for inter-procedural verification, 39-55 [Zbl 1325.68137]
Basu, Samik; Bultan, Tevfik; Ouederni, Meriem, Synchronizability for verification of asynchronously communicating systems, 56-71 [Zbl 1325.68139]
Ben-Amram, Amir M.; Genaim, Samir; Masud, Abu Naser, On the termination of integer loops, 72-87 [Zbl 1325.68056]
Bozzelli, Laura; Pinchinat, Sophie, Verification of gap-order constraint abstractions of counter systems, 88-103 [Zbl 1325.68141]
Bugaychenko, Dmitry, On application of multi-rooted binary decision diagrams to probabilistic model checking, 104-118 [Zbl 1325.68142]
Chaki, Sagar; Gurfinkel, Arie; Strichman, Ofer, Regression verification for multi-threaded programs, 119-135 [Zbl 1325.68060]
Charlton, Nathaniel; Horsfall, Ben; Reus, Bernhard, Crowfoot: a verifier for higher-order store programs, 136-151 [Zbl 1325.68143]
Chatterjee, Krishnendu; Raman, Vishwanath, Synthesizing protocols for digital contract signing, 152-168 [Zbl 1325.94115]
Dimitrova, Rayna; Finkbeiner, Bernd; Kovács, Máté; Rabe, Markus N.; Seidl, Helmut, Model checking information flow in reactive systems, 169-185 [Zbl 1326.68182]
Ermis, Evren; Hoenicke, Jochen; Podelski, Andreas, Splitting via interpolants, 186-201 [Zbl 1326.68091]
Ferrara, Pietro; Müller, Peter, Automatic inference of access permissions, 202-218 [Zbl 1326.68092]
Finkbeiner, Bernd; Jacobs, Swen, Lazy synthesis, 219-234 [Zbl 1326.68183]
Ghorbal, Khalil; Ivančić, Franjo; Balakrishnan, Gogul; Maeda, Naoto; Gupta, Aarti, Donut domains: efficient non-convex domains for abstract interpretation, 235-250 [Zbl 1326.68094]
Howar, Falk; Steffen, Bernhard; Jonsson, Bengt; Cassel, Sofia, Inferring canonical register automata, 251-266 [Zbl 1326.68168]
Kinder, Johannes; Kravchenko, Dmitry, Alternating control flow reconstruction, 267-282 [Zbl 1326.68099]
Klein, Uri; Piterman, Nir; Pnueli, Amir, Effective synthesis of asynchronous systems from GR(1) specifications, 283-298 [Zbl 1326.68186]
Lee, Woosuk; Lee, Wonchan; Yi, Kwangkeun, Sound non-statistical clustering of static analysis alarms, 299-314 [Zbl 1326.68100]
Leino, K. Rustan M., Automating induction with an SMT solver, 315-331 [Zbl 1326.68262]
Namjoshi, Kedar S.; Trefler, Richard J., Local symmetry and compositional verification, 348-362 [Zbl 1326.68103]
Oe, Duckki; Stump, Aaron; Oliver, Corey; Clancy, Kevin, versat: a verified modern SAT solver, 363-378 [Zbl 1326.68263]
Rosenberg, Stan; Banerjee, Anindya; Naumann, David A., Decision procedures for region logic, 379-395 [Zbl 1326.68264]
Sack, Joshua; Zhang, Lijun, A general framework for probabilistic characterizing formulae, 396-411 [Zbl 1326.68176]
Siegel, Stephen F.; Zirkel, Timothy K., Loop invariant symbolic execution for parallel programs, 412-427 [Zbl 1326.68106]
von Essen, Christian; Jobstmann, Barbara, Synthesizing efficient controllers, 428-444 [Zbl 1326.68190]
Zufferey, Damien; Wies, Thomas; Henzinger, Thomas A., Ideal abstractions for well-structured transition systems, 445-460 [Zbl 1326.68205]


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


Zbl 1206.68013
Full Text: DOI