Viktor Kuncak, Andrey Rybalchenko
Proceedings of the 13th International Conference on Verification, Model Checking and Abstract Interpretation
VMCAI, 2012.

@proceedings{VMCAI-2012,
	address       = "Philadelphia, Pennsylvania, USA",
	doi           = "10.1007/978-3-642-27940-9",
	editor        = "Viktor Kuncak and Andrey Rybalchenko",
	isbn          = "978-3-642-27939-3",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 13th International Conference on Verification, Model Checking and Abstract Interpretation}",
	volume        = 7148,
	year          = 2012,
}

Contents (29 items)

7 ×#verification
5 ×#source code
3 ×#automation
3 ×#named
2 ×#abstraction
2 ×#model checking
2 ×#multi
2 ×#on the
2 ×#performance
2 ×#probability

VMCAI-2012-BouajjaniDES #abstract domain #automation #infinity #reasoning #source code

Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data (AB, CD, CE, MS), pp. 1–22.

VMCAI-2012-Jhala #verification

Software Verification with Liquid Types (RJ), p. 23.

VMCAI-2012-Nipkow #education #proving #semantics

Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs (TN), pp. 24–38.

VMCAI-2012-AlbarghouthiGC #algorithm #interprocedural #named #verification

Whale: An Interpolation-Based Algorithm for Inter-procedural Verification (AA, AG, MC), pp. 39–55.

VMCAI-2012-BasuBO #communication #verification

Synchronizability for Verification of Asynchronously Communicating Systems (SB, TB, MO), pp. 56–71.

VMCAI-2012-Ben-AmramGM #integer #on the #termination

On the Termination of Integer Loops (AMBA, SG, ANM), pp. 72–87.

VMCAI-2012-BozzelliP #abstraction #constraints #verification

Verification of Gap-Order Constraint Abstractions of Counter Systems (LB, SP), pp. 88–103.

VMCAI-2012-Bugaychenko #diagrams #model checking #multi #on the #probability

On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model Checking (DB), pp. 104–118.

VMCAI-2012-ChakiGS #concurrent #multi #source code #thread #verification

Regression Verification for Multi-threaded Programs (SC, AG, OS), pp. 119–135.

VMCAI-2012-CharltonHR #higher-order #named #source code #verification

Crowfoot: A Verifier for Higher-Order Store Programs (NC, BH, BR), pp. 136–151.

VMCAI-2012-ChatterjeeR #contract #protocol

Synthesizing Protocols for Digital Contract Signing (KC, VR), pp. 152–168.

VMCAI-2012-DimitrovaFKRS #data flow #model checking

Model Checking Information Flow in Reactive Systems (RD, BF, MK, MNR, HS), pp. 169–185.

VMCAI-2012-ErmisHP

Splitting via Interpolants (EE, JH, AP), pp. 186–201.

VMCAI-2012-FerraraM #automation

Automatic Inference of Access Permissions (PF, PM), pp. 202–218.

VMCAI-2012-FinkbeinerJ #lazy evaluation #synthesis

Lazy Synthesis (BF, SJ), pp. 219–234.

VMCAI-2012-GhorbalIBMG #abstract interpretation #performance

Donut Domains: Efficient Non-convex Domains for Abstract Interpretation (KG, FI, GB, NM, AG), pp. 235–250.

VMCAI-2012-HowarSJC #automaton #canonical

Inferring Canonical Register Automata (FH, BS, BJ, SC), pp. 251–266.

VMCAI-2012-KinderK #control flow #re-engineering

Alternating Control Flow Reconstruction (JK, DK), pp. 267–282.

VMCAI-2012-KleinPP #effectiveness #specification #synthesis

Effective Synthesis of Asynchronous Systems from GR(1) Specifications (UK, NP, AP), pp. 283–298.

VMCAI-2012-LeeLY #clustering #static analysis #statistics

Sound Non-statistical Clustering of Static Analysis Alarms (WL, WL, KY), pp. 299–314.

VMCAI-2012-Leino #automation #induction #smt

Automating Induction with an SMT Solver (KRML), pp. 315–331.

VMCAI-2012-MorseVMM #c #message passing #modelling #source code

Modeling Asynchronous Message Passing for C Programs (EM, NV, EM, JM), pp. 332–347.

VMCAI-2012-NamjoshiT #composition #symmetry #verification

Local Symmetry and Compositional Verification (KSN, RJT), pp. 348–362.

VMCAI-2012-OeSOC #named #satisfiability

versat: A Verified Modern SAT Solver (DO, AS, CO, KC), pp. 363–378.

VMCAI-2012-RosenbergBN #logic

Decision Procedures for Region Logic (SR, AB, DAN), pp. 379–395.

VMCAI-2012-SackZ #framework #probability

A General Framework for Probabilistic Characterizing Formulae (JS, LZ), pp. 396–411.

VMCAI-2012-SiegelZ #execution #invariant #parallel #source code #symbolic computation

Loop Invariant Symbolic Execution for Parallel Programs (SFS, TKZ), pp. 412–427.

VMCAI-2012-EssenJ #performance

Synthesizing Efficient Controllers (CvE, BJ), pp. 428–444.

VMCAI-2012-ZuffereyWH #abstraction

Ideal Abstractions for Well-Structured Transition Systems (DZ, TW, TAH), pp. 445–460.