Welcome to the website of the International Conference on Verification, Model Checking, and Abstract Interpretation 2018.

VMCAI provides a forum for researchers from the communities of Verification, Model Checking, and Abstract Interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas. VMCAI 2018 will be the 19th edition in the series.

Proceedings

The papers will be freely available from Springer here from Jan 7 to Feb 3, 2018.

Travel Support for Students

PhD students can apply for a grant covering up to $1000 for travel and registration costs. We encourage particularly female students and underrepresented minorities to apply for this grant. Due to budget restrictions, a limited number of students can benefit from this support. Interested students must apply before Dec 10, 2017, 23:59 AoE, by sending a request to isil@cs.utexas.edu and palsberg@cs.ucla.edu mentioning their name, affiliation, contact information (address, email), and reason for applying for this grant. Applicants will be notified by Dec 15, 2017.

Dates
You're viewing the program in a time zone which is different from your device's time zone - change time zone

Conference Day
Sun 7 Jan

Displayed time zone: Tijuana, Baja California change

09:00 - 10:00
Invited Talk by Ranjit JhalaVMCAI at Watercourt
Chair(s): Isil DilligUT Austin
09:00
60m
Talk
Reasoning about Functions
VMCAI
Ranjit JhalaUniversity of California, San Diego
10:30 - 12:00
SynthesisVMCAI at Watercourt
Chair(s): K. Rustan M. LeinoAmazon
10:30
30m
Talk
Abstraction-Based Interaction Model for Synthesis
VMCAI
Hila Peleg, Shachar ItzhakyTechnion, Israel, Sharon ShohamTel Aviv university
11:00
30m
Talk
A Framework for Computer-Aided Design of Educational Domain Models
VMCAI
Eric ButlerUniversity of Washington, Emina TorlakUniversity of Washington, Zoran PopovicUniversity of Washington
11:30
30m
Talk
Generating Tests by Example
VMCAI
Hila Peleg, Dan RasinTechnion – Israel Institute of Technology, Eran YahavTechnion
14:00 - 15:30
VerificationVMCAI at Watercourt
Chair(s): Jeffrey S. FosterUniversity of Maryland, College Park
14:00
30m
Talk
Gradual Program Verification
VMCAI
Johannes BaderMicrosoft, Jonathan AldrichCarnegie Mellon University, Éric TanterUniversity of Chile
14:30
30m
Talk
A Logical System for Modular Information Flow Verification
VMCAI
Adi PrabawaNational University of Singapore, Mahmudul Faisal Al AmeenNational University of Singapore, Benedict LeeNational University of Singapore, Wei-Ngan ChinNational University of Singapore
15:00
30m
Talk
P5: Planner-less Proofs of Probabilistic Parameterized Protocols
VMCAI
16:00 - 17:30
SecurityVMCAI at Watercourt
Chair(s): Francesco RanzatoUniversity of Padova
16:00
30m
Talk
Code Obfuscation Against Abstract Model Checking Attacks
VMCAI
Roberto BruniDipartimento di Informatica, Universita' di Pisa, Roberto GiacobazziUniversity of Verona and IMDEA Software Institute, Roberta GoriDipartimento di Informatica, Universita' di Pisa
16:30
30m
Talk
Scalable Approximation of Quantitative Information Flow in Programs
VMCAI
Fabrizio BiondiCentraleSupelec Rennes, Mike EnescuINRIA, Annelie HeuserCNRS/IRISA, Axel Legay, Kuldeep S. MeelNational University of Singapore, Jean QuilbeufINRIA
17:00
30m
Talk
Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference
VMCAI
Samuele BuroUniversità degli Studi di Verona, Isabella MastroeniUniversity of Verona, Italy

Conference Day
Mon 8 Jan

Displayed time zone: Tijuana, Baja California change

09:00 - 10:00
Invited Talk by Kenneth L. McMillanVMCAI at Watercourt
Chair(s): Lenore Zuck
09:00
60m
Talk
How to Stay Decidable
VMCAI
Kenneth L. McMillanMicrosoft Research
10:30 - 12:00
Abstract InterpretationVMCAI at Watercourt
Chair(s): Patrick Cousot
10:30
30m
Talk
On Constructivity of Galois Connections
VMCAI
Francesco RanzatoUniversity of Padova
11:00
30m
Talk
An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
VMCAI
Laura TitoloNational Institute of Aerospace, USA, Marco A. FeliuNational Institute of Aerospace, Mariano MoscatoNational Institute of Aerospace, Cesar MunozNASA
11:30
30m
Talk
Modular Analysis of Executables using On-Demand Heyting Completion
VMCAI
Julian KranzTechnical University of Munich, Axel SimonGoogle
14:00 - 15:30
PotpourriVMCAI at Watercourt
Chair(s): Wei-Ngan ChinNational University of Singapore
14:00
30m
Talk
Revisiting MITL to Fix Decision Procedures
VMCAI
Nima RoohiUniversity of Pennsylvania, Mahesh ViswanathanUniversity of Illinois at Urbana-Champaign
14:30
30m
Talk
On abstraction and compositionality for weak-memory linearisability
VMCAI
Brijesh DongolBrunel University London, Radha JagadeesanDePaul University, James RielyDePaul University, Alasdair ArmstrongBrunel University
15:00
30m
Talk
Automatic Verification of RMA Programs via Abstraction Extrapolation
VMCAI
Cedric BaumannETH Zurich, Andrei Marian DanETH Zurich, Yuri MeshmanIMDEA, Torsten HoeflerETH Zurich, Martin VechevETH Zürich
16:00 - 17:30
Invited Tutorial by Mayur NaikVMCAI at Watercourt
Chair(s): Jens PalsbergUniversity of California, Los Angeles (UCLA)
16:00
90m
Talk
Maximum Satisfiability in Program Analysis: Applications and Techniques
VMCAI
Mayur NaikUniversity of Pennsylvania, Xujie SiUniversity of Pennsylvania, Xin ZhangMassachusetts Institute of Technology, USA, Radu GrigoreUniversity of Kent
18:00 - 22:00
VMCAI BanquetVMCAI at Watercourt
18:00
4h
Dinner
Banquet
VMCAI

Conference Day
Tue 9 Jan

Displayed time zone: Tijuana, Baja California change

09:00 - 10:00
Invited Talk by Azadeh FarzanVMCAI at Watercourt
Chair(s): Isil DilligUT Austin
09:00
60m
Talk
Rethinking Compositionality for Concurrent Program Proofs
VMCAI
Azadeh FarzanUniversity of Toronto
14:00 - 15:30
Types and AnalysisVMCAI at Watercourt
Chair(s): Tachio TerauchiWaseda University
14:00
30m
Talk
From Shapes to Amortized Complexity
VMCAI
Tomas FiedorVUT Brno, Lukáš HolíkBrno University of Technology, Adam RogalewiczBrno University of Technology , Moritz SinnSt. Polten University of Applied Sciences, Tomáš VojnarBrno University of Technology, Florian ZulegerTU Vienna
14:30
30m
Talk
Invariant Generation for Multi-Path Loops with Polynomial Assignments
VMCAI
Andreas HumenbergerVienna University of Technology, Maximilian JaroschekVienna University of Technology, Laura KovacsChalmers University of Technology
15:00
30m
Talk
Refinement Types for Ruby
VMCAI
Milod Kazerounian, Niki VazouUniversity of Maryland, Austin BourgerieUniversity of Maryland, Jeffrey S. FosterUniversity of Maryland, College Park, Emina TorlakUniversity of Washington
16:00 - 17:30
Model CheckingVMCAI at Watercourt
Chair(s): Kenneth L. McMillanMicrosoft Research
16:00
30m
Talk
Learning to Complement Büchi Automata
VMCAI
Yong LiInstitute of Software, Chinese Academy of Sciences, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences, Sven ScheweUniversity of Liverpool
16:30
30m
Talk
Selfless Interpolation for Infinite-State Model Checking
VMCAI
Tanja SchindlerUniversity of Freiburg, Dejan JovanovićSRI International
17:00
30m
Talk
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
VMCAI
Benjamin AminofVienna University of Technology, Sasha RubinUniversity of Naples Federico II, Ilina StoilkovskaVienna University of Technology , Josef WidderTU Wien, Florian ZulegerTU Vienna

Call for Papers

VMCAI 2018 welcomes research papers on any topic related to verification, model checking, and abstract interpretation. Research contributions can report new results as well as experimental evaluations and comparisons of existing techniques. Topics include, but are not limited to: Program Verification, Model Checking, Abstract Interpretation, Abstract Domains, Program Synthesis, Static Analysis, Type Systems, Deductive Methods, Program Logics, First-Order Theories, Decision Procedures, Interpolation, Horn Clause Solving, Program Certification, Separation Logic, Probabilistic Programming and Analysis, Error Diagnosis, Detection of Bugs and Security Vulnerabilities, Program Transformations, Hybrid and Cyber-physical Systems, Concurrent Systems, Analysis of Numerical Properties.

Submissions can address any programming paradigm, including concurrent, constraint, functional, imperative, logic, and object-oriented programming.

Submissions

Submissions are restricted to 20 pages in Springer’s LNCS format, not counting references. Additional material may be placed in an appendix, to be read at the discretion of the reviewers and to be omitted in the final version. Formatting style files and further guidelines for formatting can be found at the Springer website.

Submissions must be uploaded via the paper submission site.

Accepted papers will be published in Springer’s Lecture Notes in Computer Science series.

Accepted Papers

Title
A Framework for Computer-Aided Design of Educational Domain Models
VMCAI
A Logical System for Modular Information Flow Verification
VMCAI
Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference
VMCAI
Abstraction-Based Interaction Model for Synthesis
VMCAI
An Abstract Interpretation Framework for the Round-Off Error Analysis of Floating-Point Programs
VMCAI
Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity
VMCAI
Automatic Verification of Intermittent Systems
VMCAI
Automatic Verification of RMA Programs via Abstraction Extrapolation
VMCAI
Banquet
VMCAI

Co-Design and Verification of an Available File System
VMCAI
Code Obfuscation Against Abstract Model Checking Attacks
VMCAI
From Shapes to Amortized Complexity
VMCAI
Generating Tests by Example
VMCAI
Gradual Program Verification
VMCAI
How to Stay Decidable
VMCAI
Invariant Generation for Multi-Path Loops with Polynomial Assignments
VMCAI
Learning to Complement Büchi Automata
VMCAI
Maximum Satisfiability in Program Analysis: Applications and Techniques
VMCAI
Modular Analysis of Executables using On-Demand Heyting Completion
VMCAI
On Constructivity of Galois Connections
VMCAI
On abstraction and compositionality for weak-memory linearisability
VMCAI
P5: Planner-less Proofs of Probabilistic Parameterized Protocols
VMCAI
Parameterized Model Checking of Synchronous Distributed Algorithms by Abstraction
VMCAI
Reasoning about Functions
VMCAI
Refinement Types for Ruby
VMCAI
Rethinking Compositionality for Concurrent Program Proofs
VMCAI
Revisiting MITL to Fix Decision Procedures
VMCAI
Scalable Approximation of Quantitative Information Flow in Programs
VMCAI
Selfless Interpolation for Infinite-State Model Checking
VMCAI