Social Program
Refreshments and snacks will be offered during coffee breaks.
There will be a social dinner on Friday, organized separately for faculty and students (with the goal of getting students to meet and socialize with fellow students from other universities):
- Faculty.
Dinner at 7pm at the Edge Water Grille restaurant located at Coralville Marriott Hotel.
We reserved a private room and requested separate checks.
Transportation will be needed to get there. Free street parking is available close by. Participants can go there directly or meet the organizers at the Iowa Memorial Union parking lot, for joint departure at 6:45pm.
- Students. Students will be divided in small groups and directed to a number of restaurants in downtown Iowa City (a 5-10 minute walk from the workshop site). Groups and meeting place will be posted in the workshop room on Friday.
There is no organized lunch on Saturday.
Nearby Iowa City downtown provides a wide selection of coffeehouses and restaurants for all pockets.
Technical Program
| | |
| Friday, September 11 (Room S401 PBB) | |
| 1:50 | Welcome Address |
| 2:00 |
Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services
Hridesh Rajan, Iowa State University (talk slides) |
| 2:30 |
Behavioral Automata Composition for Automatic Topology Independent Verification of Parameterized Systems
Youssef Hanna, Iowa State University (talk slides) |
| 3:00 |
SAT Solvers and Search-Based Client Applications
Brady Garvin, University of Nebraska - Lincoln (talk slides) |
| 3:15 | Coffee Break |
| 4:00 |
Invited talk:
SMT@Microsoft
Leonardo de Moura, Microsoft Research (talk slides) |
| 5:00 |
Verifying Imperative Abstractions with Dependent and Linear Types
Aaron Stump, The University of Iowa (talk slides) |
| 5:15 |
List and Set Proofs in Guru
John Hughes and Greg Witt, The University of Iowa (talk slides) |
| 5:30 |
Fast and Flexible Proof Checking for SMT
Duckki Oe and Andy Reynolds, The University of Iowa (talk slides) |
| 7:00 | Social Dinner |
| | |
| | |
| Saturday, September 12 (Room W401 PBB) | |
| |
|
| 9:00 |
Invited Talk:
Formal Methods for Critical Systems
Steve Miller, Rockwell Collins (talk slides) |
| 10:00 |
Verifying Correctness and Reliability of Cumulative Attestation Kernels on Flash MCUs
Michael LeMay, University of Illinois at Urbana-Champaign |
| 10:30 | Coffee Break |
| 11:15 |
Scheduling Test Using Atomicity Violations
Francesco Sorrentino, University of Illinois at Urbana-Champaign (talk slides) |
| 11:30 |
Register Transfer Level Test Generation as Meta-Reasoning about Simulation
Michael Katelman, University of Illinois at Urbana-Champaign (talk slides) |
| 12:00 |
Rewriting Logic Semantics of a Plan Execution Language
Camilo Rocha, University of Illinois at Urbana-Champaign |
| 12:30 | Lunch Break |
| 2:00 |
The Linear Temporal Logic of Rewriting Model Checker
Kyungmin Bae, University of Illinois at Urbana-Champaign (talk slides) |
| 2:30 |
Verifying Tolerant Systems using Polynomial Approximations
Pavithra Prabhakar, University of Illinois at Urbana-Champaign (talk slides) |
| 3:00 |
Sireum/Topi LDP: A Lightweight Semi-Decision Procedure for Optimizing Symbolic Execution-based Analyses
Jason Belt, Kansas State University (talk slides) |
| 3:30 |
Decision Procedure for Partial Orders
Elena Sherman, University of Nebraska - Lincoln (talk slides) |
| 3:45 |
Concluding remarks Aaron Stump and Cesare Tinelli |
| 4:00 | End of Workshop |
| | |
