Clarke Symposium 2014:
Celebrating 25 Years of Model Checking

FRIDAY, 19 SEPTEMBER 2014, ASA Conference Room, 6115 Gates Hillman Center
8:00 am - 5:00 pm

8:00 - 8:45 Breakfast
8:45 - 9:00 Orna Grumberg: Opening Remarks
9:00 - 9:10 Frank Pfenning: Greetings
9:10 - 9:20 Pankaj Chauhan: Formal Verification in the Real World
9:20 - 9:30 Xiaoqing Jin: Verification and Validation Challenges in Automobiles(on behalf of Jim Kapinski)
9:30 - 9:40 Raj Rajkumar: Prof. Clarke's Impact on Automotive Systems
9:40 - 9:50 Yu-Fang Chen: Verifying Recursive Programs Using Intraprocedural Analyzers
9:50 - 10:00 Ming-Hsien Tsai (on behalf of Yih-Kuen Tsay) Verifying Curve25519 Software
10:00 - 10:10 Anvesh Komuravelli: Model Checking with Proofs and Counterexamples
10:10 - 10:20 Murali Talupur: Model Checking Distributed Protocols
10:20 - 11:00 Break
11:00 - 11:10 Daniel Kroening: Exploit-Generation with Acceleration
11:10 - 11:20 Azadeh Farzan
11:20 - 11:30 Ansgar Fehnker: The Moon and Sixpence
11:30 - 11:40 Yunshan Zhu & Yuan Lu: Assertion Synthesis
11:40 - 11:50 Rajeev Alur: Regular Functions
11:50 - 12:00 Marius Minea: Verifying Security of Web Applications and Services
12:00 - 12:10 Mike Browne: ITSPHUN demo
12:10 - 12:20 Karem Sakallah: Nobody Does It Better!
12:20 - 12:30 Xudong He: Bounded Model Checking of High Level Petri Nets
12:30 - 2:00 Lunch
2:00 - 2:10 Kenneth McMillan: Structured Decision Strategies
2:10 - 2:20 Armin Biere: SAT Based Model Checking
2:20 - 2:30 William Klieber: Solving QBF with Free Variables
2:30 - 2:40 Clark Barrett: Satisfiability Modulo Theories
2:40 - 2:50 Cesare Tinelli: SMT-Based Model Checking
2:50 - 3:00 Jeremy Avigad: The Lean Theorem Prover
3:00 - 3:40 Break
3:40 - 3:50 Natasha Sharygina: Verification of Software Upgrades
3:50 - 4:00 Somesh Jha: Some Reflections on Working with Ed Clarke
4:00 - 4:10 Natarajan Shankar: When Model Checking met Deduction
4:10 - 4:20 Sanjit A. Seshia: Integrating Induction and Deduction in Model Checking
4:20 - 4:30 Subash Shankar: A Tool for Integrating Abstract Interpretation, Model Checking, and Deductive Verification
4:30 - 4:40 Andreas Podelski: CEGAR for Black-Box System Verification
4:40 - 4:50 Aarti Gupta: Software Model Checking
4:50 - 5:00 Sagar Chaki: Model Checking Distributed Software
6:00 Dinner at local restaurants

SATURDAY, 20 SEPTEMBER 2014, ASA Conference Room, 6115 Gates Hillman Center
8:00 am - 5:00 pm

8:00 - 9:00 Breakfast
9:00 - 9:15 Helmut Veith: Opening Remarks
9:15 - 9:30 Randy Bryant: Greetings + Cloud BDDs: Mapping BDDs onto a distributed cluster
9:30 - 9:40 Gianfranco Ciardo: Unifying decision diagrams
9:40 - 9:50 Bing Liu: Parameter Identification Using Model Checking for Systems Biology
9:50 - 10:00 Jasmin Fisher: Computing Cancer
10:00 - 10:10 Michael Theobald: Formal verification of Anton, a special-purpose machine for molecular dynamics simulation
10:10 - 10:20 James R. Faeder: Model Checking Cell Decisions
10:20 - 11:00 Break
11:00 - 11:10 A. Prasad Sistla: Runtime and Static Verification of Probabilisitc Systems
11:10 - 11:20 P S Thiagarajan: Probabilistic Approximation and Verification of Hybrid Systems
11:20 - 11:30 Corina Pasareanu: On the Probabilistic Analysis of Programs
11:30 - 11:40 David Musliner & Robert P. Goldman: Probalistic Model Checking: A Decade of Uncertainty
11:40 - 11:50 Lei Bu: Online Hybrid Automata Verification of Dynamical Cyber-Physical System
11:50 - 12:00 Andre Platzer: Verified runtime validation of verified CPS models
12:00 - 12:10 Sicun Gao: Descriptive Control Theory
12:10 - 2:00 Lunch
2:00 - 2:30 Photo Session
2:30 - 2:40

Qinsi Wang: SReach: Combining SMT-based Model Checking and Statistical Tests
2:40 - 2:50 Rupak Majumdar: Language-theoretic Tools in Model Checking
2:50 - 3:00 Scott Smolka: Linear Model measurements with Application to Bird Flocking
3:00 - 3:30 Break
3:30 - 3:40 Patrice Godefroid: Dynamic Software Model Checking
3:40 - 3:50 Masahiro Fujita: Formal Analysis with Small Numbers of Test Vectors
3:50 - 4:00 David Brumley: Checking the World's Software for Exploitable Bugs
4:00 - 4:10 Rance Cleaveland: On-the-fly Model Checking
4:10 - 4:20 Karsten Wolf: Model Checking Petri Nets
4:20 - 4:30 Jin Song Dong: Event Analytics and Verification
4:30 - 4:40 Edmund M. Clarke: Concluding Remarks
6:30 - 9:30 Banquet at Wyndham Hotel

Home