19th International Conference on Verification, Model Checking, and Abstract InterpretationVMCAI 2018
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.
Sun 7 Jan Times are displayed in time zone: Tijuana, Baja California change
09:00 - 10:00 Talk | Reasoning about Functions VMCAI Ranjit JhalaUniversity of California, San Diego |
10:30 - 11:00 Talk | Abstraction-Based Interaction Model for Synthesis VMCAI | ||
11:00 - 11:30 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 - 12:00 Talk | Generating Tests by Example VMCAI |
14:00 - 15:30: VerificationVMCAI at Watercourt Chair(s): Jeffrey S. FosterUniversity of Maryland, College Park | |||
14:00 - 14:30 Talk | Gradual Program Verification VMCAI | ||
14:30 - 15:00 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 - 15:30 Talk | P5: Planner-less Proofs of Probabilistic Parameterized Protocols VMCAI |
16:00 - 16:30 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 - 17:00 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 - 17:30 Talk | Abstract Code Injection - A Semantic Approach Based on Abstract Non-Interference VMCAI |
Mon 8 Jan Times are displayed in time zone: Tijuana, Baja California change
09:00 - 10:00 Talk | How to Stay Decidable VMCAI Kenneth L. McMillanMicrosoft Research |
10:30 - 11:00 Talk | On Constructivity of Galois Connections VMCAI Francesco RanzatoUniversity of Padova | ||
11:00 - 11:30 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 - 12:00 Talk | Modular Analysis of Executables using On-Demand Heyting Completion VMCAI |
14:00 - 14:30 Talk | Revisiting MITL to Fix Decision Procedures VMCAI | ||
14:30 - 15:00 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 - 15:30 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 - 17:30 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 Dinner | Banquet VMCAI |
Tue 9 Jan Times are displayed in time zone: Tijuana, Baja California change
09:00 - 10:00 Talk | Rethinking Compositionality for Concurrent Program Proofs VMCAI Azadeh FarzanUniversity of Toronto |
10:30 - 12:00: Verifying Protocols and SystemsVMCAI at Watercourt Chair(s): James RielyDePaul University | |||
10:30 - 11:00 Talk | Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity VMCAI | ||
11:00 - 11:30 Talk | Automatic Verification of Intermittent Systems VMCAI | ||
11:30 - 12:00 Talk | Co-Design and Verification of an Available File System VMCAI |
14:00 - 14:30 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 - 15:00 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 - 15:30 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 - 16:30 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 - 17:00 Talk | Selfless Interpolation for Infinite-State Model Checking VMCAI | ||
17:00 - 17:30 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.