|
AFM
|
CICLOPS
|
ESCoR
|
GDV
|
ICLP
|
MVLPA
|
PDPAR
|
PLPV
|
SVV
|
TV
|
UITP
|
V&D
|
WG
|
| |
| |
|
|
|
|
|
|
|
|
08:30‑09:00 (Metropolitan A)
Robert Cook
Thread Verification an experience report
|
|
08:30‑09:15 (Suite 3128)
John Moondanos
From Error to Error: Debugging in the Era of Multi-core Designs
|
|
09:00‑09:30 (Suite 3228)
John Rushby
Overview of PVS, ICS, and SAL, and plans for the future [pdf]
|
09:00‑10:00 (Suite 2828)
Matt Kaufmann
Maintaining the ACL2 Theorem Proving System [pdf]
|
09:00‑10:30 (Suite 2802)
ICLP Doctoral Student Consortium |
09:00‑10:00 (Richmond)
Peter Dybjer
Programming Languages Meet Program Verification [pdf]
|
09:00‑09:30 (Metropolitan A)
Arndt Mühlenfeld
and Franz Wotawa
Fault Detection in Multi-Threaded C++ Server Applications
|
09:00‑09:30 (Suite 2628)
Julien Narboux
A Graphical User Interface for Formal Proofs in Geometry.
|
09:00‑10:30 (Pacific)
WG 1.7 Meeting |
09:15‑09:30 (Suite 3028)
Welcoming Remarks
|
09:15‑10:00 (Suite 3128)
Alper Sen
Error Diagnosis in Equivalence Checking of High Performance Microprocessors
|
09:30‑10:00 (Suite 3228)
Sam Owre
Recent PVS Language Developments [pdf]
|
09:30‑10:30 (Suite 2928)
Neng-Fa Zhou
AR (Action Rules): The Language, Implementation, and Applications [ppt]
|
09:30‑10:30 (Suite 3102)
Luca de Alfaro
Interface theories in practice [ppt]
|
09:30‑10:30 (Metropolitan B)
Peter O'Hearn
Proof Procedures for Separated Heap Abstractions
|
09:30‑10:30 (Suite 3028)
Byron Cook
Automatic Termination Proofs for Systems-level Code [ppt]
|
09:30‑10:30 (Metropolitan A)
Maurice Herlihy
What Can We Prove about Transactional Memory? [ppt]
|
09:30‑10:00 (Suite 2628)
Pedro Quaresma
and Predrag Janicic
GeoThms - a Web System for Euclidean Constructive Geometry
|
10:00‑10:30 (Suite 3228)
N. Shankar
Recent PVS Prover Developments [pdf]
|
10:00‑10:30 (Suite 2828)
Virgile Prevosto and Uwe Waldmann
SPASS+T
|
10:00‑10:30 (Richmond)
James Caldwell
and Josef Pohl
Constructive membership predicates as index types
|
10:00‑10:30 (Suite 2628)
Claudio Sacerdoti Coen
, Enrico Tassi
and Stefano Zacchiroli
Tinycals: step by step tacticals
|
10:00‑10:30 (Suite 3128)
Lionel van den Berg, Paul Strooper
and Wendy Johnston
An Automated Approach for the Interpretation of Counter-Examples
|
10:30‑11:00
Break |
11:00‑11:30 (Suite 3228)
Leonardo de Moura
Overview of ICS/Yices [pdf]
|
11:00‑11:30 (Suite 2928)
Ricardo Rocha
Efficient Support for Incomplete and Complete Tables in the YapTab Tabling System
|
11:00‑11:30 (Suite 2828)
Petr Pudlak
Search for faster and shorter proofs using machine generated lemmas
|
11:00‑12:00 (Suite 3102)
Marcin Jurdzinski
Algorithms for solving parity games [pdf]
|
11:00‑12:30 (Suite 2802)
ICLP Doctoral Student Consortium |
|
11:00‑11:30 (Metropolitan B)
Sava Krstic
, Robert Jones
and John O'Leary
Mothers of Pipelines
|
11:00‑11:30 (Richmond)
Martin Sulzmann and Razvan Voicu
Language-Based Program Verification via Expressive Types
|
11:00‑11:30 (Suite 3028)
Ganna Zaks
and Amir Pnueli
Translation Validation of Interprocedural Optimizations
|
11:00‑11:30 (Metropolitan A)
Alexander Malkis
, Andreas Podelski and Andrey Rybalchenko
Thread-Modular Verification and Cartesian Abstraction
|
11:00‑11:30 (Suite 2628)
Cezary Kaliszyk
Web Interfaces for Proof Assistants
|
11:00‑11:30 (Suite 3128)
Jooyong Lee
Dynamic Reverse Code Generation for Backward Execution
|
11:00‑12:30 (Pacific)
WG 1.7 Meeting (continued) |
11:30‑12:00 (Suite 3228)
John Rushby
Overview of SAL: Model Checking and Test Generation [pdf]
|
11:30‑12:00 (Suite 2928)
Remko Troncon
, Bart Demoen and Gerda Janssens
When tabling does not work
|
11:30‑12:00 (Suite 2828)
Jia Meng
and Lawrence Paulson
Lightweight Relevance Filtering for Machine-Generated Resolution
|
11:30‑12:00 (Suite 3002)
Ajay Mallya
Horn-based Multi-Valued Verification
|
11:30‑12:00 (Metropolitan B)
Swen Jacobs
and Viorica Sofronie-Stokkermans
Applications of hierarchical reasoning in the verification of complex systems
|
11:30‑12:00 (Richmond)
Oleg Kiselyov and Chung-chieh Shan
Lightweight static capabilities
|
11:30‑12:00 (Suite 3028)
Luke Simon, Ajay Mallya, Ajay Bansal and Gopal Gupta
Co-Logic Programming: Extending Logic Programming with Coinduction
|
11:30‑12:00 (Metropolitan A)
Chiara Braghin and Natasha Sharygina
Modeling and Verification of Mobile Systems
|
11:30‑12:00 (Suite 2628)
Marc Wagner
, Serge Autexier
and Christoph Benzmüller
PLATO: A Mediator between Text-Editors and Proof Assistance Systems
|
11:30‑12:30 (Suite 3128)
Andreas Zeller
Where Do Bugs Come From? [pdf]
|
12:00‑12:30 (Suite 3228)
Bruno Dutertre
Model Checking Infinite-state Systems in SAL [pdf]
|
12:00‑12:30 (Suite 2928)
Hai-Feng Guo
and Miao Liu
Embedding Solution Preferences via Transformation
|
12:00‑12:15 (Suite 2828)
Jia Meng
and Lawrence Paulson
Translating Higher-Order Problems to First-Order Clauses
|
|
12:00‑12:30 (Suite 3002)
Zoran Majkic
Functional Many-valued Logic and Global Predicate Compression
|
12:00‑12:15 (Metropolitan B)
Ofer Strichman
and Daniel Kroening
A Framework for Decision Procedures in Program Verification
|
12:00‑12:30 (Richmond)
Louis-Julien Guillemette and Stefan Monnier
Statically Verified Type-Preserving Code Transformations in Haskell
|
|
12:00‑12:30 (Metropolitan A)
Frederic Dabrowski and Frederic Boussinot
Cooperative threads and preemptive computations
|
|
| |
12:15‑12:30 (Metropolitan B)
Geoffrey Brown and Lee Pike
Easy Parameterized Verificaton of Biphase Mark and 8N1 Protocols
|
12:30‑14:00
Lunch break |
14:00‑15:00 (Suite 3228)
Joseph Kiniry
(Deeply) Integrating Programming and Proving [pdf]
|
14:00‑14:30 (Suite 2928)
Bart Demoen
and Phuong-Lan Nguyen
Delay and events in the TOAM and the WAM
|
14:00‑15:00 (Suite 2828)
Johan Bos
Three Stories on Automated Reasoning for Natural Language Understanding [ppt]
|
14:00‑14:45 (Suite 3102)
Barbara Jobstmann and Roderick Bloem
Game-based and simulation-based improvements for LTL synthesis
|
14:00‑15:30 (Suite 2802)
ICLP Doctoral Student Consortium |
14:00‑15:00 (Suite 3002)
Michael Gelfond
Probabilistic Reasoning with Answer Sets
|
14:00‑15:00 (Metropolitan B)
Koen Claessen
The Power of Finite Model Finding [ppt]
|
14:00‑14:30 (Richmond)
Tim Sheard
Type-level Computation Using Narrowing in Omega
|
14:00‑14:30 (Suite 3028)
Aleks Zaks, Ilya Shlyakhter
, Franjo Ivancic, Srihari Cadambi, Zijiang Yang, Malay Ganai, Aarti Gupta and Pranav Ashar
Using Range Analysis for Software Verification
|
14:00‑14:30 (Metropolitan A)
Lukasz Ziarek, Philip Schatz and Suresh Jagannathan
Modular Checkpointing for Atomicity
|
14:00‑14:30 (Suite 2628)
Anne Mulhern
, Charles Fischer
and Ben Liblit
Tool Support for Proof Engineering
|
14:00‑15:00 (Suite 3128)
Wolfgang Mayer and Markus Stumptner
Model-Based Debugging -- State of the Art And Future Challenges
|
14:00‑15:30 (Pacific)
WG 1.7 Meeting (continued) |
14:30‑15:00 (Suite 2928)
Tiago Soares
, Michel Ferreira, Ricardo Rocha
and Nuno Fonseca
On Applying Deductive Databases to Inductive Logic Programming: a Performance Study
|
14:30‑15:00 (Richmond)
Andreas Schlosser
, Christoph Walther
, Michael Gonder and Markus Aderhold
Context-Dependent Procedures and Computed Types in VeriFun
|
14:30‑15:00 (Suite 3028)
Elvira Albert
, Miguel Gómez-Zamalloa, Laurent Hubert
and German Puebla
Java Bytecode Verification using
Analysis and Transformation of Logic Programs
|
14:30‑15:30 (Metropolitan A)
Nir Shavit
Transactional Locking
|
14:30‑15:00 (Suite 2628)
Josef Urban
and Grzegorz Bancerek
Presenting and Explaining Mizar
|
14:45‑15:30 (Suite 3102)
Krishnendu Chatterjee, Thomas A. Henzinger and Nir Piterman
Algorithms for Büchi games
|
15:00‑15:30 (Suite 3228)
Cesar Munoz
Batch Proving and Proof Scripting in PVS [pdf]
|
15:00‑15:30 (Suite 2928)
Quan Phan
and Gerda Janssens
Towards Region-based Memory Management for Mercury Programs
|
15:00‑15:30 (Suite 2828)
Michael Wessel
and Ralf Moeller
A Flexible DL-based Architecture for Deductive Information Systems
|
15:00‑15:30 (Suite 3002)
Rajesh Kumar
, Ashish Tiwari
and Bruce Krogh
EOLC: Efficiently Modelling Inconsistency for Commonsense Reasoning
|
15:00‑15:15 (Metropolitan B)
Chao Wang
, Aarti Gupta and Malay Ganai
Predicate Learning and Selective Theory Deduction for Solving Difference Logic
|
15:00‑15:30 (Richmond)
Brigitte Pientka
Functional programming with higher-order abstract syntax and
explicit substitution
|
15:00‑15:30 (Suite 3028)
Stefano Tonetta and Natasha Sharygina
A Uniform Framework for Predicate Abstraction Approximation
|
15:00‑15:30 (Suite 2628)
Steven Trac
, Yury Puzis
and Geoff Sutcliffe
An Interactive Derivation Viewer
|
15:00‑15:30 (Suite 3128)
Irith Pomeranz and Sudhakar Reddy
On the Use of Functional Test Generation in Diagnostic Test Generation for Synchronous Sequential Circuits
|
15:15‑15:30 (Metropolitan B)
Silvio Ghilardi
, Enrica Nicolini, Silvio Ranise
and Daniele Zucchelli
Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies
|
15:30‑16:00
Break |
16:00‑16:30 (Suite 3228)
Chris George and Anne E. Haxthausen
Specification and Proof of the Mondex Electronic Purse
|
16:00‑16:30 (Suite 2928)
Pedro Costa, Ricardo Rocha
and Michel Ferreira
DBTAB: a Relational Storage Model for the YapTab Tabling System
|
16:00‑16:30 (Suite 2828)
Gerd Beuster, Niklas Henrich and Markus Wagner
Real World Verification - Experiences from the Verisoft Email Client
|
16:00‑17:00 (Suite 3102)
Christof Löding
Memory reduction for strategies in infinite games [pdf]
|
16:00‑17:00 (Suite 2802)
ICLP Doctoral Student Consortium |
16:00‑16:30 (Suite 3002)
Ajay Mallya
Four-Valued Models and Abstract Game Structures
|
16:00‑16:30 (Metropolitan B)
Behzad Akbarpour
and Lawrence Paulson
Towards Automatic Proofs of Inequalities Involving Elementary Functions
|
16:00‑16:15 (Richmond)
Aaron Stump
The Alternation Calculus
|
16:00‑16:30 (Suite 3028)
Achim D. Brucker
and Burkhart Wolff
A Package for Extensible Object-Oriented Data Models with an Application to IMP++
|
16:00‑17:00 (Metropolitan A)
Wolfram Schulte and Bart Jacobs
A simple sequential reasoning approach for sound modular verification of mainstream multithreaded programs. [ppt]
|
16:00‑16:30 (Suite 2628)
Peter C. Dillinger
, Panagiotis Manolios
, Daron Vroon
and J Strother Moore
ACL2s: "The ACL2 Sedan"
|
16:00‑16:30 (Suite 3128)
Andreas Griesmayer, Stefan Staber and Roderick Bloem
Automated Fault Localization for C Programs
|
16:00‑18:00 (Pacific)
WG 1.7 Meeting (continued) |
16:15‑16:30 (Richmond)
Adam Chlipala
Position Paper: Thoughts on Programming with Proof Assistants
|
16:30‑17:00 (Suite 3228)
Borzoo Bonakdarpour and Sandeep S. Kulkarni
Mechanical Verification of Automated Synthesis of Multitolerance
|
16:30‑17:00 (Suite 2928)
Lukas Chrpa
Linear Logic: Foundations, Applications and Implementations
|
16:30‑16:45 (Suite 2828)
Florian Rabe
Towards Determining the Subset Relation between Propositional Modal Logics
|
16:30‑17:00 (Suite 3002)
Alan Bond
A distributed modular logic programming model based on the cortex
|
16:30‑17:00 (Metropolitan B)
Maria Paola Bonacina
and Mnacho Echenim
Rewrite-Based Satisfiability Procedures for Recursive Data Structures
|
16:30‑17:15 (Richmond)
Panel Discussion: Future Directions of Language-Based Program Verification |
16:30‑17:00 (Suite 3028)
Dieu Donne Okalas Ossami, Jeanine Souquieres and Jean-Pierre Jacquot
Ensuring Specifications Correctness by Construction
|
16:30‑17:00 (Suite 2628)
Louise Abigail Dennis
Enhancing Theorem Prover Interfaces with Program Slice Information
|
16:30‑17:30 (Suite 3128)
Martin Rinard
Automated Techniques for Surviving Software Errors [ppt]
|
16:45‑17:00 (Suite 2828)
Gonçalo Lopes
and Luís Moniz Pereira
Prospective Logic Programming with ACORDA
|
17:00‑17:30 (Suite 3228)
Paul Nicholas Loewenstein, Shailender Chaudhry, Robert Cypher and Chaiyasit Manovit
Multiprocessor Memory Model Verification
|
|
17:00‑17:15 (Suite 2828)
Matthias Baaz
, Stefan Hetzl, Alexander Leitsch
, Clemens Richter
and Hendrik Spohr
System Description: The Cut-Elimination System CERES
|
|
|
17:00‑17:30 (Suite 3002)
Andrew Mironov and Virendra Bhavsar
Fuzzy Modal Logics
|
17:00‑17:30 (Metropolitan B)
Clark Barrett
, Igor Shikanian
and Cesare Tinelli
An Abstract Decision Procedure for Satisfiability in the Theory of Recursive Data Types
|
|
17:00‑18:00 (Metropolitan A)
Moderated 5-minute sessions open to all attendees
|
17:00‑18:00 (Suite 2628)
Session 5: Discussion, Demos, Business Meeting |
17:15‑17:30 (Suite 2828)
Boontawee Suntisrivaraporn
, Franz Baader
and Carsten Lutz
CEL---A Short System Demonstration
|
|
17:30‑18:00 (Suite 3228)
Sam Owre
Random Testing in PVS
|
17:30‑18:30 (Suite 2828)
Matt Kaufmann, Boris Motik, Michael Norrish, Cesare Tinelli
My Top Ten Things To Do for more Empirically Successful Computerized Reasoning
|
|
17:30‑17:45 (Metropolitan B)
Silvio Ranise
, Christophe Ringeissen
and Duc-Khanh Tran
Producing Conflict Sets for Combinations of Theories
|
17:30‑18:00 (Suite 3128)
Juan Carlos López Pimentel
, Raúl Monroy
and Dieter Hutter
A method for patching interleaving-replay attacks in faulty security protocols
|
17:45‑18:30 (Metropolitan B)
Discussion
|
| |
|
|
|
|
