[Om-announce] Call for Participation -- CAV 2008
Aarti Gupta
agupta at nec-labs.com
Fri May 9 18:42:58 CEST 2008
We apologize if you receive multiple copies of this email. See below on
how to unsubscribe.
..............................................................
CALL FOR PARTICIPATION
Early Registration Deadline: May 25, 2008
CAV 2008
20th International Conference on Computer Aided Verification
http://www.princeton.edu/cav2008
July 7 - 14, 2008 Princeton, NJ, USA
..............................................................
CAV 2008 is the 20th in a series dedicated to the advancement of the
theory and practice of computer-aided formal analysis methods for
hardware and software systems.
***** Invited Talks
- James Larus (Microsoft): Singularity: Designing Better Software
- Edmund M. Clarke (CMU), E. Allen Emerson (UT Austin), Joseph Sifakis
(CNRS)
- Edward Felten (Princeton): Coping with Outside-the-Box Attacks
***** Invited Tutorials (July 9)
- Harry Foster (Mentor Graphics): Assertion-based Verification
- John Harrison (Intel): Theorem Proving for Verification
- Peter O' Hearn (University of London): Tutorial on Separation Logic
- Reinhard Wilhelm (Saarland University): Abstract Interpretation with
Applications to Timing Validation
***** Affiliated Events
- First CAV Award Presentation
- SMT Competition
- Hardware Model Checking Competition
***** Affiliated Workshops
- Exploiting Concurrency Efficiently and Correctly (EC2)^2: July 7 and 8
http://www.cs.utah.edu/ec2
- Satisfiability Modulo Theories (SMT): July 7 and 8
http://research.microsoft.com/conferences/SMT08/
- Numerical abstractions for Software Verification (NSV): July 8
http://theory.stanford.edu/~srirams/nsv/index.html
- Automated Formal Methods (AFM): July 14
http://fm.csl.sri.com/AFM08/
- Bit-Precise Reasoning (BPR): July 14
http://www.cs.ubc.ca/~babic/index_bpr.htm
- Formal verification of Analog Circuits (FAC): July 14
http://www.em.informatik.uni-frankfurt.de/FAC08.html
- Heap Analysis and Verification (HAV): July 14
http://research.microsoft.com/~jjb/HAV2008/index.html
***** Social Events
- Conference Reception: July 9
- Conference Banquet: July 10
- Manhattan Cruise Excursion: July 12
***** Registration Deadlines
Early registration: May 25
Regular registration: June 21
Late registration: After June 21 and on-site
Please follow directions and links on conference website.
***** Accommodations
CAV has arranged special rates at nearby hotels for conference
participants. Dorm rooms on Princeton University campus are also
available. Please follow directions and links on conference website.
***** Advance Program (Conference)
----- July 9 (Wednesday) Tutorials Day
8:45 - 9:00 Opening Remarks
9:00 - 10:30 Harry Foster: Assertion-based Verification
10:30 - 11:00 Break I
11:00 - 12:30 John Harrison: Theorem Proving for Verification
12:30 - 2:00 Lunch
2:00 - 3:30 Peter O'Hearn: Tutorial on Separation Logic
3:30 - 4:00 Break II
4:00 - 5:30 Reinhard Wilhelm: Abstract Interpretation with
Applications to Timing Validation
6:00 - 7:30 Conference Reception
----- July 10 (Thursday)
8:45 - 9:00 Opening Remarks
9:00 - 10:00 Invited Talk: James Larus -- Singularity: Designing
Better Software
10:00 - 10:30 Break I
10:30 - 12:30 Session 1: Concurrency
10:30 Akash Lal and Thomas Reps: Reducing Concurrent Analysis Under a
Context Bound to Sequential Analysis
11:00 Azadeh Farzan and P. Madhusudan: Monitoring Atomicity in
Concurrent Programs
11:30 Sarvani Vakkalanka, Ganesh Gopalakrishnan and Robert Kirby:
Dynamic Verification of MPI programs with Reductions in Presence of
Split Operations and Relaxed Orderings
12:00 Naoki Kobayashi and Davide Sangiorgi: A Hybrid Type System for
Lock-Freedom of Mobile Processes
12:30 - 2:00 Lunch
2:00 - 3:30 Session 2: Memory Consistency
2:00 Surender Baswana and Shashank Mehta: Implied Set Closure and Its
Application to Memory Consistency Verification
2:30 Sebastian Burckhardt and Madanlal Musuvathi: Effective Program
Verification for Relaxed Memory Models
3:00 Ariel Cohen, Amir Pnueli and Lenore Zuck: Mechanical
Verification of Transactional Memories with Non-Transactional Memory
Accesses
3:30 - 4:00 Break II
4:00 - 5:30 Special Session
ACM 2007 Turing Award Winners: Edmund Clarke, Allen Emerson, Joseph
Sifakis
6:30 - 10:30 Conference Banquet at Institute for Advanced Study,
Princeton
----- July 11 (Friday)
9:00 - 10:30 Session 3: Abstraction/Refinement
9:00 Mihaela Gheorghiu Bobaru, Corina Pasareanu and Dimitra
Giannakopoulou: Automated Assume-Guarantee Reasoning by Abstraction
Refinement
9:30 Ariel Cohen and Kedar Namjoshi: Local Proofs for Linear-Time
Properties of Concurrent Programs
10:00 Holger Hermanns, Bjorn Wachter and Lijun Zhang: Probabilistic
CEGAR
10:30 - 11:00 Break I
11:00 - 12:00 Session 4: Hybrid Systems
11:00 Andre Platzer and Edmund Clarke: Computing Differential Invariants
of Hybrid Systems as Fixedpoints
11:30 Sumit Gulwani and Ashish Tiwari: Constraint-based Approach for
Analysis of Hybrid Systems
12:00 - 12:30 Session 5: Tools - Dynamic Verification
12:00 Ambar Gadkari, Anand Yeolekar, J Suresh, Ramesh S, Swarup Kumar
Mohalik and K.C. Shashidhar: AutoMOTGen: Automatic Model Oriented Test
Generator for Embedded Control Systems
12:15 Andreas Holzer, Christian Schallhart, Michael Tautschnig and
Helmut Veith: FShell: Systematic Test Case Generation for Dynamic
Analysis and Measurement
12:30 - 2:00 Lunch
2:00 - 3:30 Session 6: Modeling and Specification Formalisms
2:00 Salil Joshi and Barbara Konig: Applying the Graph Minor Theorem
to the Verification of Graph Transformation Systems
2:30 Deepak D'Souza and Madhu Gopinathan: Conflict-Tolerant Features
3:00 Rajeev Alur, Aditya Kanade and Gera Weiss: Ranking Automata and
Games for Prioritized Requirements
3:30 - 4:00 Break II
4:00 - 5:30 Session 7: Decision Procedures
4:00 Himanshu Jain, Edmund Clarke and Orna Grumberg: Efficient
Interpolation for Linear Diophantine (Dis)equations and Linear Modular
Equations
4:30 Ruzica Piskac and Viktor Kuncak: Linear Arithmetic with Stars
5:00 Andy King and Harald Sondergaard: Inferring Congruence Equations
with SAT
5:30 - 6:30 Session 8: Tools - Decision Procedures
5:30 Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric
Rodriguez Carbonell and Albert Rubio: The Barcelogic SMT solver
5:45 Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto
Griggio and Roberto Sebastiani: The MathSAT 4 SMT Solver
6:00 Dirk Beyer, Damien Zufferey and Rupak Majumdar: CSIsat:
Interpolation for LA+EUF
6:15 Laura Meikle and Jacques Fleuriot: Prover's Palette: A
User-Centric Approach to Verification with Isabelle and QEPCAD
6:30 - 7:30 CAV Business Meeting
----- July 12 (Saturday)
9:00 - 10:00 Invited Talk: Edward Felten -- Coping with
Outside-the-Box Attacks
10:00 - 10:30 Break I
10:30 - 12:30 Session 9: Program Verification
10:30 Andreas Podelski, Andrey Rybalchenko and Thomas Wies: Heap
Assumptions On Demand
11:00 Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko and
Mooly Sagiv: Proving Conditional Termination
11:30 Parosh Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frederic
Haziza and Ahmed Rezine: Monotonic Abstraction for Programs with Dynamic
Memory Heaps
12:00 Huu Hai Nguyen and Wei-Ngan Chin: Enhancing Program Verification
with Lemmas
12:30 - 1:30 Lunch
1:30 - 3:00 Session 10: Program and Shape Analysis
1:30 Bhargav Gulavani and Sumit Gulwani: A Numerical Abstract Domain
based on "Expression Abstraction" and "Max Operator" with Application in
Timing Analysis
2:00 Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno,
Byron Cook, Dino Distefano and Peter O'Hearn: Scalable Shape Analysis
For Systems Code
2:30 Josh Berdine, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam and
Mooly Sagiv: Thread Quantification for Concurrent Shape Analysis
3:00 - 3:30 Break II
3:30 - 4:30 Session 11: Tools - Security and Program
Analysis
3:30 Cas Cremers: The Scyther Tool: Verification, Falsification, and
Analysis of Security Protocols
3:45 Michael Backes, Stefan Lorenz, Matteo Maffei and Kim Pecina: The
CASPA Tool: Causality-based Abstraction for Security Protocol Analysis
4:00 Johannes Kinder and Helmut Veith: Jakstab: A Static Analysis
Platform for Binaries
4:15 Stephen Magill, Ming-Hsien Tsai, Peter Lee and Yih-Kuen Tsay:
THOR: A Tool for Reasoning about Shape and Arithmetic
4:45 - 11:45 Manhattan Cruise Excursion
------ July 13 (Sunday) Last day of Conference
9:00 - 10:00 Session 12: Hardware Verification I
9:00 Cindy Eisner, Amir Nahir and Karen Yorav: Functional Verification
of Power Gated Designs by Compositional Reasoning
9:30 Per Bjesse: A Practical Approach to Word Level Model Checking of
Industrial Netlists
10:00 - 10:30 Break I
10:30 - 11:45 Session 13: Hardware Verification II
10:30 Sudipta Kundu, Sorin Lerner and Rajesh Gupta: Validating High
Level Synthesis
11:00 Oliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz
and Gert-Martin Greuel: An algebraic approach for proving data
correctness in arithmetic data paths
11:30 Kavita Ravi, Hyondeuk Kim, Hoonsang Jin, Petr Spacek, Robert P.
Kurshan, Fabio Somenzi and John Pierce: Application of Formal Word-Level
Analysis in Constrained Random Simulation
11:45 - 12:00 Hardware Model Checking Competition Report
12:00 - 12:15 SMT-Comp Report
12:15 - 2:00 Lunch
2:00 - 3:00 Session 14: Model Checking
2:00 Sujatha Kashyap and Vijay Garg: Producing short counterexamples
using "crucial events"
2:30 Peter Niebert, Doron Peled and Amir Pnueli: Discriminative Model
Checking
3:00 - 4:00 Session 15: Space Efficient Algorithms
3:00 Pavel Simecek, Stefan Edelkamp and Peter Sanders: Semi-External
LTL Model Checking
3:30 Rob van Glabbeek and Bas Ploeger: Correcting a Space-Efficient
Simulation Algorithm
4:00 - 4:30 Break II
4:30 - 5:15 Session 16: Tools - Model Checking
4:30 Simon Gay, Rajagopal Nagarajan and Nikolaos Papanikolaou: QMC: A
Model Checker for Quantum Systems
4:45 Axel Legay: T(O)RMC: A Tool for (Omega)-Regular Model Checking
5:00 Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel and Andreas
Podelski: Faster than Uppaal?
5:15 End of Conference
***** Program Committee
- Rajeev Alur, University of Pennsylvania
- Nina Amla, Cadence
- Clark Barrett, New York University
- Armin Biere, JKU Linz
- Roderick Bloem, TU Graz
- Ahmed Bouajjani, University Paris 7
- Alessandro Cimatti, IRST Trento
- Werner Damm, Oldenburg University
- Steven German, IBM
- Ganesh Gopalakrishnan, University of Utah
- Mike Gordon, University of Cambridge
- Orna Grumberg, Technion
- Aarti Gupta (co-chair), NEC Labs America
- David Harel, Weizmann Institute
- John Harrison, Intel
- Thomas A. Henzinger, EPFL
- Holger Hermanns, Saarland University
- Pei-Hsin Ho, Synopsys
- Robert Jones, Intel
- Daniel Kroening, Oxford University
- Orna Kupferman, Hebrew University
- Shuvendu Lahiri, Microsoft Research
- Rupak Majumdar, University of California - Los Angeles
- Oded Maler, Verimag
- Sharad Malik (co-chair), Princeton University
- Ken McMillan, Cadence
- Kedar Namjoshi, Bell Labs, Alcatel-Lucent
- Corina Pasareanu, NASA
- Amir Pnueli, New York University
- Andreas Podelski, University of Freiburg
- Shaz Qadeer, Microsoft Research
- Koushik Sen, University of California - Berkeley
- Fabio Somenzi, University of Colorado
- Ofer Strichman, Technion
- Karen Yorav, IBM Haifa
- Lenore Zuck, University of Illinois
***** Program Chairs
- Aarti Gupta, NEC Labs America
- Sharad Malik, Princeton University
***** Organizing Committee
- Workshops Chair: Byron Cook, Microsoft Research
- Tutorials Chair: Alan Hu, University of British Columbia
***** Local Arrangements
- Webmaster: Nadia Papakonstantinou, NEC Labs America
- Campus Arrangements:
- Tara R. Zarillo, Princeton University
- Stacey Weber Jackson, Princeton University
- Hospitality Crew:
- NEC Labs Verification Group
- Princeton Malik Group
***** Steering Committee
- Edmund M. Clarke, Carnegie Mellon University
- Mike Gordon, University of Cambridge
- Robert P. Kurshan, Cadence
- Amir Pnueli, New York University
***** Sponsors
- Princeton University (http://www.princeton.edu)
- Cadence (http://www.cadence.com)
- IBM (http://www.ibm.com)
- Intel (http://www.intel.com)
- Jasper Design Automation (http://www.jasper-da.com)
- Mentor Graphics (http://www.mentor.com)
- Microsoft Research (http://research.microsoft.com)
- NEC Labs America (http://www.nec-labs.com)
- Synopsys (http://www.synopsys.com)
........................................................................
.
We apologize if you receive multiple copies of this email. If you do not
want any further announcements regarding CAV 2008, reply to this email
and put 'UNSUBSCRIBE' in the body or subject of your reply.
More information about the Om-announce
mailing list