AISB Convention 2015

The AISB Convention is an annual conference covering the range of AI and Cognitive Science, organised by the Society for the Study of Artificial Intelligence and Simulation of Behaviour. The 2015 Convention will be held at the Uni...


Read More...

Yasemin Erden on BBC

AISB Committee member, and Philosophy Programme Director and Lecturer, Dr Yasemin J. Erden interviewed for the BBC on 29 October 2013. Speaking on the Today programme for BBC Radio 4, as well as the Business Report for BBC world N...


Read More...

Mark Bishop on BBC ...

Mark Bishop, Chair of the Study of Artificial Intelligence and the Simulation of Behaviour, appeared on Newsnight to discuss the ethics of ‘killer robots’. He was approached to give his view on a report raising questions on the et...


Read More...

AISB YouTube Channel

The AISB has launched a YouTube channel: http://www.youtube.com/user/AISBTube (http://www.youtube.com/user/AISBTube). The channel currently holds a number of videos from the AISB 2010 Convention. Videos include the AISB round t...


Read More...

Lighthill Debates

The Lighthill debates from 1973 are now available on YouTube. You need to a flashplayer enabled browser to view this YouTube video  


Read More...
01234

Notice

AISB event Bulletin Item

CF Participation: Computer Aided Verification CAV 2008

http://www.princeton.edu/cav2008

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)