The meeting will be held at
Kansas State University in the
Tadtman Boardroom and Engineering Hall 1109,
Manhattan KS 66506.

The ninth Midwest Verification Day (MVD 2017) will be held at the Kansas State University, Manhattan, Kansas on October 6-7, 2017, continuing the tradition of MVD 2009-MVD 2016. Midwest Verification Day is an informal annual regional workshop on hardware and software verification, with verification understood in a broad sense. Topics of interest include, but are not limited to, deductive verification, model checking, static analysis, abstract interpretation, runtime verification, model-based testing, and security. The workshop seeks to provide a forum for students and researchers to present their work and ideas to workshop participants in an informal and relaxed setting and share suggestions and ideas on other participants’ work, early drafts of papers, and presentations.

The workshop has no proceedings, and papers in progress and/or submitted/accepted elsewhere are welcome. Participation is open to anyone and there are no registration fees. Thus, anyone willing to give talk is encouraged to do so. A number of student travel and accommodation grants are available. Students requesting travel support should indicate this at the time of registration.

Important Dates

  • September 5, 2017: Deadline for registration. The registration/submission page is now open.
  • September 25, 2017: Announcement of the final program.
  • October 6-7, 2017: The workshop will be held at Kansas State University, Manhattan, Kansas.



  • Ratan Lal

Past Editions

  • MVD 2016, Iowa State University, Ames, Iowa
  • MVD 2015, University of Illinois, Urbana-Champaign
  • MVD 2014, University of Missouri, Columbia
  • MVD 2013, University of Illinois, Chicago
  • MVD 2012, University of Kansas, Lawrence
  • MVD 2011, University of Minnesota, Minneapolis
  • MVD 2010, University of Iowa, Iowa City
  • MVD 2009, University of Iowa, Iowa City
  • MVD for more details about Midwest Verification Day
Friday October 6, Tadtman Boardroom 100
8:00 to 8:50 Breakfast
8:50 to 9:00 Opening remarks
9:00 to 10:00
Chair: Pavithra Prabhakar
Kenneth McMillan Keynote: Compositional Testing (abstract)
10:00 to 10:30 Break
10:30 to 12:00
Chair: Ratan Lal
Jianwen Li SAT-based explicit LTLf satisfiability checking (abstract)
Hao Ren RELIQE: REduced Logic Inference using Quantifier Elimination for Compositional Reasoning of Time-dependent Contracts (abstract)
Yanjun Wang A Decidable Logic for Tree Data-Structures with Measurements (abstract)
12:00 to 1:30 Lunch
1:30 to 3:00
Chair: Torben Amtoft
Hariharan Thiagarajan Risk Analysis for Medical Device Systems of Systems (abstract)
Kangjing Huang DryadSynth : A Concolic SyGuS Solver (abstract)
Samantha Syeda Khairunnesa Exploiting Implicit Beliefs to Resolve Sparse Usage Problem in Usage-based Specification Mining (abstract)
3:00 to 3:30 Break
3:30 to 5:30
Chair: Omar Chowdhury
Zhongkai Wen Intrusion Detection: Beyond Ground Truth (abstract)
Yiji Zhang An LLVM Refinement Checker and its Applications(abstract)
Joydeep Mitra Ghera: A Repository of Android App Vulnerability Benchmarks (abstract)
Ajay Kumar Eeralla Mechanized Analysis of Vote Privacy using Computationally Complete Symbolic Attacker (abstract)
Saturday October 7, Engineering Hall 1109
8:00 to 9:00 Breakfast
9:00 to 10:00
Chair: Cesare Tinelli
Raymond Richards Keynote: Design and Verification of System Cyber Resiliency (abstract)
10:00 to 10:30 Break
10:30 to 12:00
Chair: Perry Alexander
Swarn Priya A Mechanized Core Calculus for Message Passing Concurrency (abstract)
Zhen Yu Dynamic Detection of Mixed Deadlocks Based on Lock Allocation Graphs (abstract)
Denis Bueno EUForia: Syntactic Abstraction and Verification of C Programs with Incremental Induction (abstract)

Kenneth McMillan (Microsoft Research) on Friday at 9:00 a.m.
Title:Compositional Testing
Abstract: While full formal proof of complex systems remains a challenge, formal methods can readily be applied in practice to improve the performance of testing in exposing design errors. A good example of this is compositional testing. In this methodology each component of a system is given a formal specification and it is proved formally that these specifications guarantee system-level correctness. The components are then rigorously tested against their formal specifications. This approach has the advantages of unit testing in covering component behaviors, while at the same time exposing all system-level errors to testing. Moreover, it can expose latent bugs in components that are not stimulated in the given system but may occur when the component is re-used in a different environment. This talk will cover the basics of compositional testing and discuss some industrial applications.

Biography: Ken McMillan is a principal researcher at Microsoft Research in Redmond, Washington. He works in formal verification, primarily in model checking for hardware and software. He holds a BS in electrical engineering from the University of Illinois at Urbana (1984), an MS in electrical engineering from Stanford (1986) and a Ph.D. in computer science from Carnegie Mellon (1992). He is the author of the book "Symbolic Model Checking", and the SMV symbolic model checking system. For his work in model checking, he has received the ACM doctoral dissertation award, the SRC technical excellence award, the ACM Paris Kannelakis award, the Alan Newell award from Carnegie Mellon and the Computer-aided Verification Conference award. He was formerly a member of the technical staff at AT&T Bell Laboratories and a fellow at Cadence research labs.

Raymond Richards (DARPA) on Saturday at 9:00 a.m.
Title: Design and Verification of System Cyber Resiliency
Abstract: This talk will begin with a short discussion of DARPA’s history, mission, and structure.
The state-of-the-art in systems engineering is very adept at engineering systems for a variety of non-functional properties. These properties include such things as reliability, durability, availability, etc. Colloquially, these properties, which include safety and performance, are known as the –ilities. Unfortunately, cyber properties are not included in the systems engineering domain. A new program at DARPA is looking to advance the state-of-the-art in formal methods technologies to allow systems to be designed for cyber resiliency. This talk will highlight the technical challenges and the approached being developed by the Cyber Assured Systems Engineering (CASE) program.

Biography: Dr. Raymond (“Ray”) Richards joined DARPA in January 2016. His research interests focus on high assurance software and systems.
Dr. Richards joined DARPA from Rockwell Collins Advanced Technology Center (ATC) where he led a research group focused on automated analysis, cyber, and information assurance. In this role he helped to foster the industrial use of formal methods verification to support security accreditations. He also served as the liaison to U.S. Government S&T funding agencies for Rockwell Collins. He has performed research in the formal modeling and analysis of high assurance systems. He led the software development for a high-assurance cross-domain guard, and the formal modeling and analysis effort of a real-time operating system, in support of a Common Criteria EAL6+ evaluation. Dr. Richards has over 20 years of experience in leading the development of state-of-the-art computer hardware, software and systems. Dr. Richards has experience in developing real-time software ranging from high fidelity ground vehicle simulators, to developing safety critical software for air transport category aircraft.
Dr. Richards holds an MBA degree, Ph.D. and M.S. degrees in Electrical and Computer Engineering, and a B.S. degree in Electrical Engineering, all from the University of Iowa. He has several publications in the area of formal methods/software security analysis and one patent.

The meeting will be held at Kansas State University in the following two locations:
  • Friday October 6, 2017, Tadtman Boardroom, 100 Alumni Center, 1720 Anderson Avenue, Manhattan, KS 66506.
  • Saturday October 7, 2017, Lecture room Engineering Hall 1109, 1701D Platt Street Manhattan, KS 66506.
  • More information about traveling to Kansas State University can be found here.


    The rooms have been blocked in the following hotels for MVD until September 15, 2017 (Fairfield Inn Marriott) and October 5, 2017 (Candlewood Suites) (Check-out on the 7th).

    The registration is free. Note that after submitting the registration form, you will get a notification email for confirmation. If you do not receive a notification email, please contact us.
    2184 Engineering Hall
    1701D Platt St.
    Manhattan, KS 66506
    Phone: 785-532-6350

    Sponsored By

    RockwellCollinsLogo     toyota-logo      cs