We apologize if you receive multiple copies of this email. See below on how to unsubscribe.
..............................................................
CAV 2008: Call For Participation =20 Early Registration to CLOSE on Tuesday, May 27, 2008=20
Hotel Room Block CUTOFF Date Wednesday, June 4, 2008 =09 20th International Conference on Computer Aided Verification http://www.princeton.edu/cav2008 July 7 - 14, 2008 Princeton, NJ, USA =20 ..............................................................
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=20
***** 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 =20 ***** 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 27 Regular registration: June 21 Late registration: After June 21 and on-site=20 Please follow directions and links on conference website.
***** Accommodations CAV has arranged special rates at nearby hotels for conference participants. The cutoff date for Nassau Inn is June 4, and for Hyatt Regency is June 6. Dorm rooms on Princeton University campus are also available.=20 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 =20 ----- July 10 (Thursday) =09 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=20 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, Shashank Mehta and Vishal Powar: Implied Set Closure and Its Application to Memory Consistency Verification=20 2:30 Sebastian Burckhardt and Madanlal Musuvathi: Effective Program Verification for Relaxed Memory Models=20 3:00 Ariel Cohen, Amir Pnueli and Lenore Zuck: Mechanical Verification of Transactional Memories with Non-Transactional Memory Accesses=20 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=20 =20 ----- 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=20 9:30 Ariel Cohen and Kedar Namjoshi: Local Proofs for Linear-Time Properties of Concurrent Programs=20 10:00 Holger Hermanns, Bjorn Wachter and Lijun Zhang: Probabilistic CEGAR=20 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=20
12:00 - 12:30 Session 5: Tools - Dynamic Verification=20 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=20 12:15 Andreas Holzer, Christian Schallhart, Michael Tautschnig and Helmut Veith: FShell: Systematic Test Case Generation for Dynamic Analysis and Measurement=20 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=20 2:30 Deepak D'Souza and Madhu Gopinathan: Conflict-Tolerant Features=20 3:00 Rajeev Alur, Aditya Kanade and Gera Weiss: Ranking Automata and Games for Prioritized Requirements=20 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=20 4:30 Ruzica Piskac and Viktor Kuncak: Linear Arithmetic with Stars=20 5:00 Andy King and Harald Sondergaard: Inferring Congruence Equations with SAT=20
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=20 5:45 Roberto Bruttomesso, Alessandro Cimatti, Anders Franzen, Alberto Griggio and Roberto Sebastiani: The MathSAT 4 SMT Solver=20 6:00 Dirk Beyer, Damien Zufferey and Rupak Majumdar: CSIsat: Interpolation for LA+EUF=20 6:15 Laura Meikle and Jacques Fleuriot: Prover's Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD=20
6:30 - 7:30 CAV Business Meeting =20 ----- July 12 (Saturday)=09 9:00 - 10:00 Invited Talk: Edward Felten -- Coping with Outside-the-Box Attacks=20 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=20 11:00 Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko and Mooly Sagiv: Proving Conditional Termination=20 11:30 Parosh Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frederic Haziza and Ahmed Rezine: Monotonic Abstraction for Programs with Dynamic Memory Heaps=20 12:00 Huu Hai Nguyen and Wei-Ngan Chin: Enhancing Program Verification with Lemmas=20 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=20 2:00 Hongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano and Peter O'Hearn: Scalable Shape Analysis For Systems Code=20 2:30 Josh Berdine, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam and Mooly Sagiv: Thread Quantification for Concurrent Shape Analysis=20 3:00 - 3:30 Break II
3:30 - 4:30 Session 11: Tools - Security and Program Analysis=20 3:30 Cas Cremers: The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols=20 3:45 Michael Backes, Stefan Lorenz, Matteo Maffei and Kim Pecina: The CASPA Tool: Causality-based Abstraction for Security Protocol Analysis=20 4:00 Johannes Kinder and Helmut Veith: Jakstab: A Static Analysis Platform for Binaries=20 4:15 Stephen Magill, Ming-Hsien Tsai, Peter Lee and Yih-Kuen Tsay: THOR: A Tool for Reasoning about Shape and Arithmetic=20
4:45 - 11:45 Manhattan Cruise Excursion =20 ------ 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=20 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=20 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=20 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=20
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"=20 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=20 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=20 4:45 Axel Legay: T(O)RMC: A Tool for (Omega)-Regular Model Checking=20 5:00 Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel and Andreas Podelski: Faster than Uppaal?=20
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)
........................................................................ .=20 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.
============================================================================== Message: Address: Action: help majordomo(a)clip.dia.fi.upm.es Info. on useful commands subscribe ciao-users-request(a)clip.dia.fi.upm.es Subscribe to this list unsubscribe ciao-users-request(a)clip.dia.fi.upm.es Unsubscribe from this list <whatever> ciao-users(a)clip.dia.fi.upm.es Send message to list ----------------------------------------------------------------------------- Archived messages: http://www.clip.dia.fi.upm.es/Mail/ciao-users/ -----------------------------------------------------------------------------