Social Program

Refreshments and snacks will be offered during coffee breaks.

There will be a social dinner at 7pm on Friday, organized separately for students and non-students---with the separation aiming at getting students to meet and socialize with fellow students from other universities:

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.

Faculty, postdocs and professionals. Dinner at 7pm at the Edge Water Grille restaurant located at Coralville Marriott Hotel. We have reserved a semi-private room and requested separate checks.
Transportation will be needed to get there. Free street parking is available close by. Attendees willing to participate can go there directly or meet the organizers at the Iowa Memorial Union parking lot, for joint departure at 6:45pm.

There is no organized lunch on Friday and Saturday. Nearby downtown Iowa City provides a wide selection of coffeehouses and restaurants for all pockets.

Technical Program

Friday, September 17    (Room S401 PBB)

08:55 Welcome Address
09:00 Algebraic-Geometric Techniques for Verification of Non-Linear Hybrid Systems
Sriram Sankaranarayanan, University of Colorado at Boulder

09:30 A dynamic analysis to explore scopes of programmer reasoning
Devin Coughlin, University of Colorado at Boulder
(talk slides)

09:45 Challenges Implementing a HOL System in Haskell or:
How I Learned to Stop Worrying and Love the Monad

Evan Austin, The University of Kansas
(talk slides)

10:00 Comparing Proof Systems for Linear Real Arithmetic with LFSC
Andrew Reynolds, The University of Iowa
(talk slides)

10:30 Coffee Break
11:00 Compositionality Entails Sequentializability
Pranav Garg, University of Illinois at Urbana-Champaign
(talk slides)

11:30 Simulation-based Verification of Hardware with Strategies
Michael Katelman, University of Illinois at Urbana-Champaign
(talk slides)

12:00 Developing a competitive SAT solver with correctness verified
Duccki Oe, The University of Iowa
(talk slides)

12:15 Increasing path-coverage of predictive analysis
Robert Frohardt, University of Colorado at Boulder

12:30 Lunch Break
02:00 The K Framework and a Formal Semantics of C
Chucky Ellison, University of Illinois at Urbana-Champaign
(talk slides)

02:15 Matching Logic: An Alternative to Hoare Logic
Andrei Stefanescu, University of Illinois at Urbana-Champaign
(talk slides)

02:30 Translucid Contracts: Expressive Specification and
Modular Verification for Aspect-Oriented Interfaces

Mehdi Bagherzadeh, Iowa State University
(talk slides)

03:00 Composition in the State-Based Rosetta Domain
Nicolas Frisby, The University of Kansas

03:15 Coffee Break
04:00 Invited talk: Is Java ready for Real-time?
Jan Vitek, Purdue University
(talk slides)

05:00 Automating Cut-off for Multi-Parameterized Systems
Youssef Hanna, Iowa State University
(talk slides)

05:30 Streett complementation made tight
Ting Zhang, Iowa State University
(talk slides)

05:45 End of technical program
07:00 Social Dinner


Saturday, September 18    (Room W151 PBB)

09:00 Invited talk: Staged Concurrent Program Analysis
Nishant Sinha, NEC Labs
(talk slides)

09:45 Specification-based testing for refinement
Teme Kahsai, The University of Iowa
(talk slides)

10:00 Smarter Load Test Suite Generation with Input Selection Support
Pingyu Zhang, University of Nebraska, Lincoln
(talk slides)

10:30 Coffee Break
11:00 Decidable logics combining heap structures and data
Xiaokang Qiu, University of Illinois at Urbana-Champaign
(talk slides)

11:30 Least and greatest fixed points
David Baelde, University of Minnesota
(talk slides)

11:45 Higher-Order Encodings in Intensional Type Theory
Edwin Westbrook, Rice University
(talk slides)

12:00 Concluding remarks
Aaron Stump and Cesare Tinelli

12:10 End of MVD
01:30 IEEE workshop talks

05:30 End of IEEE Workshop

Copyright © The University of Iowa, 2010. All Rights Reserved.
Last Modified: Sep 12, 2010. Developed and maintained by Cesare Tinelli.