|
25MC
|
ACL
|
ALPSWS
|
CAV
|
DISPROVING
|
FATES-RV
|
FCS-ARSPA
|
ICLP
|
IJCAR
|
LFMTP
|
LaSh
|
PREFS
|
Strategies
|
VERIFY
|
WLPE
|
WST
|
| |
| |
|
|
|
|
|
|
|
|
|
|
08:00‑08:15 (Suite 3028)
Welcome and Introduction
|
|
|
|
|
08:15‑09:00 (Suite 3028)
Haifeng Guo
Logic Programming with Solution Preferences [ppt]
|
08:50‑09:00 (Suite 3002)
Opening Remarks
|
09:00‑09:30 (Metropolitan A)
Edmund Clarke
The Birth of Model Checking [ppt]
|
09:00‑09:30 (Metropolitan B)
Erik Reeber
and Jun Sawada
Combining ACL2 and an Automated Verification Tool to Verify a Multiplier
|
09:00‑09:30 (Willow A)
Thomas Eiter
, Giovambattista Ianni, Roman Schindlauer
, Hans Tompits and Kewen Wang
Forgetting in Managing Rules and Ontologies
|
09:00‑10:00 (Richmond)
Jian Zhang
Model and Counterexample Search: Successes and Challenges [pdf]
|
09:00‑10:00 (Cirrus)
Martin Abadi
Access Control in a Core Calculus of Dependency [ppt]
|
09:00‑09:30 (Suite 3228)
Alwen Tiu
A Logic for Reasoning about Generic Judgments
|
09:00‑09:50 (Suite 3002)
Mirek Truszczynski
Knowledge representation languages --- a programmer's interface to satisfiability [pdf]
|
09:00‑09:30 (Suite 3028)
Alessandra Mileo
and Torsten Schaub
Extending Ordered Disjunctions for Policy Enforcement: Preliminary report
|
09:15‑09:30 (Suite 2928)
Introductory Remarks |
09:30‑10:00 (Metropolitan A)
E. Allen Emerson
The Beginnings of Model Checking: A Personal Perspective
|
09:30‑10:00 (Metropolitan B)
Ruben Gamboa
and John Cowles
Implementing a Cost-Aware Evaluator for ACL2 Expressions
|
09:30‑10:00 (Willow A)
Edna Ruckhaus
, Maria-Esther Vidal and Eduardo Ruiz
Query Evaluation and Optimization in the Semantic Web
|
09:30‑10:30 (Suite 2828)
Oege de Moor
Aspects for Trace Monitoring [pdf]
|
09:30‑10:00 (Suite 3228)
Ulrich Schoepp
Modelling Generic Judgements
|
09:30‑10:00 (Suite 3028)
Pallavi Tambay and Bharat Jayaraman
Relaxation in Preference Logic Programs
|
09:30‑10:30 (Suite 2928)
Georges Gonthier
Internal Deduction and Decision Procedures of the 4-Colour Theorem [ppt]
|
09:30‑10:30 (Suite 3128)
Christoph Walther
Verification in the Classroom
|
09:30‑10:30 (Suite 2628)
Yuri Gurevich
Program termination and well partial orderings [ppt]
|
09:50‑10:10 (Suite 3002)
Enrico Giunchiglia
, Yuliya Lierler, Marco Maratea and Armando Tacchella
Experiments with SAT-based Answer Set Programming
|
10:00‑10:30 (Metropolitan A)
Bob Kurshan
25 Years of Computer-Aided Verification [pdf]
|
10:00‑10:30 (Metropolitan B)
Robert S. Boyer
and Warren A. Hunt, Jr.
Function Memoization and Unique Object Representation for ACL2 Functions
|
10:00‑10:30 (Willow A)
Thomas Eiter
, Giovambattista Ianni, Roman Schindlauer
and Hans Tompits
dlvhex: A Tool for Semantic-Web Reasoning under the Answer-Set Semantics
|
10:00‑10:30 (Richmond)
Thomas Hillenbrand
, Dalibor Topic and Christoph Weidenbach
Sudokus as Logical Puzzles
|
10:00‑10:30 (Cirrus)
Mathieu Jaume
and Charles Morisset
Towards a formal specification of access control
|
10:00‑10:30 (Suite 3228)
Murdoch Gabbay
Hierarchical nominal rewriting
|
10:00‑10:30 (Suite 3028)
James Delgrande, Torsten Schaub
and Hans Tompits
A Preference-Based Framework for Updating Logic Programs: Preliminary Report
|
10:10‑10:30 (Suite 3002)
Maarten Mariën, Johan Wittocx and Marc Denecker
The IDP framework for declarative problem solving
|
10:30‑11:00
Break |
11:00‑11:30 (Metropolitan A)
Gerard Holzmann
New Challenges in Model Checking [pdf]
|
11:00‑11:15 (Metropolitan B)
David L. Rager
Adding Parallelism Capabilities to ACL2
|
11:00‑11:30 (Willow A)
Stijn Heymans, Livia Predoiu, Cristina Feier, Jos de Bruijn and Davy Van Nieuwenborgh
G-Hybrid Knowledge Bases
|
|
11:00‑11:30 (Richmond)
André Rognes
Automated relative consistency proving
|
11:00‑11:30 (Suite 2828)
Moez Krichen
and Stavros Tripakis
State-Identification Problems for Finite-State Transducers
|
11:00‑11:30 (Cirrus)
Amit Walvekar, Manasi Kelkar
, Melanie Smith and Rose Gamble
Determining Conflicts in Interdomain Mappings for Access Control
|
|
|
11:00‑11:30 (Suite 3228)
Stefan Berghofer
and Christian Urban
A Head-to-Head Comparison of de Bruijn Indices and Names
|
11:00‑11:40 (Suite 3002)
Ilka Niemela
Answer Set Programming: Foundations, Implementation Techniques, and Applications [pdf]
|
11:00‑11:30 (Suite 3028)
Toshiko Wakaki and Kazuo Tomita
Compiling Prioritized Circumscription into General Disjunctive Programs
|
11:00‑11:30 (Suite 2928)
Adam Chlipala
and George Necula
Cooperative Integration of an Interactive Proof Assistant and an Automated Prover
|
11:00‑12:00 (Suite 3128)
Luca Vigano
Automated Reasoning for Security Protocol Analysis [pdf]
|
|
11:00‑11:30 (Suite 2628)
Harald Zankl, Nao Hirokawa and Aart Middeldorp
Constraints for Argument Filterings
|
11:15‑11:30 (Metropolitan B)
Sandip Ray
Quantification in Tail-recursive Function Definitions
|
11:30‑12:00 (Metropolitan A)
David Dill
A Retrospective on Murphi [ppt]
|
11:30‑11:45 (Metropolitan B)
Warren A. Hunt, Jr.
and Serita M. Nelesen
Phylogenetic Trees in ACL2
|
11:30‑12:00 (Willow A)
Viviana Mascardi
and Giovanni Casella
Intelligent Agents that Reason about Web Services: a Logic Programming Approach
|
11:30‑12:00 (Richmond)
Lee Pike
, Paul Miner
and Wilfredo Torres-Pomales
Diagnosing a Failed Proof in Fault-Tolerance: A Disproving Challenge Problem
|
11:30‑12:00 (Suite 2828)
Roy Armoni, Dmitry Korchemny, Andreas Tiemeyer, Moshe Y. Vardi and Yael Zbar
Deterministic Dynamic Monitors for Linear-Time Assertions
|
11:30‑12:00 (Cirrus)
A. Prasad Sistla and Min Zhou
Analysis of Dynamic Policies
|
11:30‑12:00 (Suite 3228)
Brian Aydemir
, Aaron Bohannon
and Stephanie Weirich
Nominal Reasoning Techniques in Coq
|
11:30‑12:00 (Suite 3028)
Tu Phan, Tran Son and Enrico Pontelli
Planning with Preferences Using Constraint Logic Programming
|
11:30‑12:00 (Suite 2928)
Hongping Lim and Myla Archer
Translation Templates to Support Strategy Development in PVS
|
11:30‑12:00 (Suite 2628)
Harald Zankl and Aart Middeldorp
KBO as a Satisfaction Problem
|
11:40‑12:20 (Suite 3002)
John Franco
Experiences in the Research and Development of a Non-Clausal SAT Solver
|
11:45‑12:00 (Metropolitan B)
Matt Kaufmann
and J Strother Moore
Double Rewriting for Equivalential Reasoning in ACL2
|
12:00‑12:30 (Metropolitan A)
Rajeev Alur
Model Checking: From Tools to Theory [ppt]
|
12:00‑12:05 (Metropolitan B)
Bill Bevier and David Russinoff
Formally Modeling the x86 Instruction Set Architecture
|
12:00‑12:30 (Willow A)
Srividya Kona, Ajay Bansal, Gopal Gupta
and Thomas Hite
Efficient Web Service Discovery and Composition using Constraint Logic Programming
|
12:00‑12:30 (Richmond)
Markus Aderhold
, Christoph Walther
, Daniel Szallies and Andreas Schlosser
A Fast Disprover for VeriFun
|
12:00‑12:30 (Suite 2828)
Georgios Fainekos
and George Pappas
Robustness of Temporal Logic Specifications
|
12:00‑12:30 (Cirrus)
Chamseddine Talhi, Nadia Tawbi and Mourad Debbabi
Execution Monitoring Enforcement Under Memory-Limitation Constraints
|
12:00‑12:30 (Suite 3228)
Jason Hickey
, Aleksey Nogin
, Xin Yu and Alexei Kopylov
Practical Reflection for Sequent Logics
|
12:00‑12:30 (Suite 3028)
Mauricio Osorio and Claudia Zepeda
Preferences for General Theories in Answer Sets
|
12:00‑12:30 (Suite 2928)
Florent Kirchner and Cesar Munoz
PVS#: Streamlined Tacticals for PVS
|
12:00‑12:30 (Suite 3128)
Siraj Shaikh
, Vicky Bush and Steve Schneider
A heuristic for constructing rank functions to verify authentication protocols
|
12:00‑12:30 (Suite 2628)
Michael Codish, Peter Schneider-Kamp
, Vitaly Lagoon, Rene Thiemann
and Juergen Giesl
Automating Dependency Pairs Using SAT Solvers
|
12:05‑12:10 (Metropolitan B)
Warren Hunt
BDDs
|
12:10‑12:15 (Metropolitan B)
Peter Dillinger, Pete Manolios, J Strother Moore, and Daron Vroon
ACL2s: The ACL2 Sedan
|
12:15‑12:20 (Metropolitan B)
J Strother Moore
Semi-Automatic Functional Instantiation
|
12:20‑12:25 (Metropolitan B)
David Russinoff
A Unified Mathematical Theory of Register-Transfer Logic and Computer Arithmetic
|
|
12:25‑12:30 (Metropolitan B)
Matt Kaufmann, Pete Manolios, J Strother Moore, and Daron Vroon
Adding Calling Context Graphs to ACL2 for Improved Termination Analysis
|
12:30‑14:00 (Metropolitan A)
The winners of the 1998 and 2006 ACM Kanellakis awards
25MC Lunch/Panel: Verification in the Next 25 Years
|
12:30‑14:00
Lunch break |
12:30‑14:00
Lunch break |
12:30‑14:00
Lunch break |
12:30‑14:00
Lunch break |
12:30‑14:00
Lunch break |
12:30‑14:00
Lunch break |
12:30‑14:00
Lunch break |
|
12:30‑14:00
Lunch break |
12:30‑14:00
Lunch break |
12:30‑14:00
Lunch break |
12:30‑14:00
Lunch break |
14:00‑14:30 (Metropolitan A)
Thomas Henzinger
From Graph Models to Game Models [ppt]
|
14:00‑14:30 (Metropolitan B)
Dale Vaillancourt
, Rex Page and Matthias Felleisen
ACL2 in DrScheme
|
14:00‑14:30 (Willow A)
Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, Marco Montali and Paolo Torroni
Policy-based reasoning for smart web service interaction
|
14:00‑15:00 (Richmond)
Silvio Ranise
Satisfiability Solving for Program Verification: towards the efficient combination of Automated Theorem Provers and Satisfiability Modulo Theory Tools [pdf]
|
14:00‑14:30 (Suite 2828)
Tayfun Elmas, Shaz Qadeer
and Serdar Tasiran
Goldilocks: Efficiently Computing the Happens-Before Relation Using Locksets
|
14:00‑14:30 (Cirrus)
Veronique Cortier
and Graham Steel
On the Decidability of a Class of XOR-based Key-management APIs
|
14:00‑15:00 (Suite 3228)
Gordon Plotkin
An Algebraic Framework for Logics and Type Theories
|
14:00‑14:50 (Suite 3002)
Henry Kautz
Deconstructing Planning as Satisfiability [ppt]
|
14:00‑14:30 (Suite 2928)
Moa Johansson, Alan Bundy
and Lucas Dixon
Best-First Rippling
|
|
14:00‑14:30 (Suite 3028)
Remko Troncon
and Gerda Janssens
A Delta Debugger for ILP Query Execution
|
14:00‑14:30 (Suite 2628)
Matt Kaufmann
, Panagiotis Manolios
, J Strother Moore
and Daron Vroon
Integrating CCG Analysis into ACL2
|
14:30‑15:00 (Metropolitan A)
Limor Fix
Accelerating the Industrial Deployment of Model-Checking for SW Verification: Lessons from 10 years of Model-Checking Deployment for HW Verification in Intel [ppt]
|
14:30‑15:00 (Metropolitan B)
Jared Davis
Reasoning about ACL2 File Input
|
14:30‑15:00 (Willow A)
Posters and Demos
|
14:30‑15:00 (Suite 2828)
Cormac Flanagan
and Stephen N. Freund
Dynamic Architecture Extraction
|
14:30‑15:00 (Cirrus)
Massimo Benerecetti
, Nicola Cuomo and Adriano Peron
Timed HLPSL for specification and verification of time sensitive protocols
|
14:30‑15:00 (Suite 2928)
Maria Paola Bonacina
and Mnacho Echenim
Rewrite-Based Decision Procedures
|
14:30‑15:00 (Suite 3128)
Viorica Sofronie-Stokkermans
Local reasoning in verification
|
14:30‑15:00 (Suite 3028)
Pierre DERANSART
On using Tracer Driver for External Dynamic Process Observation (extended abstract)
|
14:30‑15:00 (Suite 2628)
Frederic Blanqui
, Adam Koprowski
, Solange Coupet-Grimal
, William Delobel and Sebastien Hinderer
CoLoR, a Coq library on Rewriting and termination
|
14:50‑15:10 (Suite 3002)
Martin Gebser
and Torsten Schaub
Characterizing ASP Inferences by Unit Propagation
|
15:00‑15:30 (Metropolitan A)
Randy Bryant
A View from the Engine Room: Computational Support for Symbolic Model Checking [ppt]
|
15:00‑15:30 (Metropolitan B)
Erik Reeber
and Warren A. Hunt, Jr.
A SAT-Based Procedure for Verifying Finite State Machines in ACL2
|
15:00‑15:30 (Willow A)
Open space: Introduction and Topic finding
|
15:00‑15:30 (Richmond)
Louise Abigail Dennis
Program Slicing and Middle-Out Reasoning for Error Location and Repair
|
15:00‑15:30 (Suite 2828)
Fabrice Bouquet
, Frederic Dadeau
, Julien Groslambert
and Jacques Julliand
Safety Property Driven Test Generation from JML Specifications
|
15:00‑15:30 (Cirrus)
Alan Jeffrey
and Ruy Ley-Wild
Dynamic Model Checking of C Cryptographic Protocol Implementations
|
15:00‑15:30 (Suite 3228)
Andrew Appel
and Xavier Leroy
A List-machine Benchmark for Mechanized Metatheory
|
15:00‑15:30 (Suite 2928)
William McCune
Semantic Guidance with Carefully Chosen Interpretations
|
15:00‑15:30 (Suite 3128)
Andreas Schlosser
, Christoph Walther
and Markus Aderhold
Axiomatic Specifications in VeriFun
|
15:00‑15:30 (Suite 3028)
Hani Girgis
and Bharat Jayaraman
A Logic-based Debugger for Java
|
15:00‑15:30 (Suite 2628)
Johannes Waldmann
Free SCC Analysis via Constant Interpretations
|
15:10‑15:30 (Suite 3002)
John Schlipf
and Ryan Flannery
Unfounded Sets and Autarkies
|
15:30‑16:00
Break |
16:00‑16:30 (Metropolitan A)
Ken McMillan
The Evolution of Symbolic Model Checking [ppt]
|
16:00‑16:45 (Metropolitan B)
Matt Kaufmann, J Strother Moore, All
Discussion on Possible Future Enhancements to ACL2
|
16:00‑17:00 (Willow A)
Open-Space, part I
|
|
16:00‑16:30 (Richmond)
Mahadevan Subramaniam, Deepak Kapur and Stephan Falke
Predicting Failures of Inductive Proof Attempts
|
16:00‑16:30 (Suite 2828)
Margus Veanes
, Pritam Roy and Colin Campbell
Online Testing with Reinforcement Learning
|
16:00‑17:00 (Cirrus)
Session 8: Discussion and conclusion |
|
|
16:00‑16:30 (Suite 3228)
Kevin Donnelly
and Hongwei Xi
A Formalization of Strong Normalization for Simply-Typed Lambda-Calculus and System F
|
16:00‑16:20 (Suite 3002)
Murray Patterson
, Yongmei Liu, Eugenia Ternovska and Arvind Gupta
Grounding for Model Expansion in $k$-Guarded Formulas
|
|
16:00‑17:00 (Suite 2928)
José Meseguer
Specifying and Implementing Strategies in Rewriting Logic [pdf]
|
16:00‑18:00 (Suite 3128)
Session 8: Panel discussion: "What are the verification problems? What are the deduction techniques?" |
16:00‑16:30 (Suite 3028)
Edison Mera, Pedro Lopez-Garcia
, German Puebla, Manuel Carro and Manuel Hermenegildo
Combining Static Analysis and Profiling for Estimating Execution Times in Logic Programs
|
16:00‑16:30 (Suite 2628)
Andreas Weiermann
Phase transition phenomena in the context of termination problems
|
16:20‑16:40 (Suite 3002)
Johannes Oetsch, Martina Seidl, Hans Tompits and Stefan Woltran
ccT: A Tool for Checking Advanced Correspondence Problems in Answer-Set Programming
|
16:30‑17:00 (Metropolitan A)
Moshe Y. Vardi
From Church and Prior to PSL [pdf]
|
16:30‑17:00 (Richmond)
Peter Baumgartner
, Alexander Fuchs
, Cesare Tinelli
and Hans de Nivelle
Computing Finite Models by Reduction to Function-Free Clause Logic
|
16:30‑17:30 (Suite 2828)
Session 10: Tool Demos |
16:30‑17:00 (Suite 3228)
Chad E. Brown
Encoding Functional Relations in Scunak
|
16:30‑17:00 (Suite 3028)
Michael Hanus
CurryBrowser: A Generic Analysis Environment for Curry Programs
|
16:30‑18:30 (Suite 2628)
System Demonstrations |
16:40‑17:00 (Suite 3002)
Lengning Liu
and Mirek Truszczynski
Solving Optimization Problems with Boolean Combinations of Pseudo-boolean Constraints (a preliminary report)
|
16:45‑17:30 (Metropolitan B)
Pete Manolios, Matt Wilding, All
Business Meeting
|
17:00‑17:30 (Metropolitan A)
Amir Pnueli
The Merits of Temporal Testers: Transducers Compose while Acceptors Do Not [pdf]
|
17:00‑18:00 (Willow A)
Open-Space, part II
|
|
|
17:00‑17:30 (Suite 3228)
Mircea Dan Hernest
Synthesis of moduli of uniform continuity by the Monotone Dialectica Interpretation in the proof-system MinLog
|
|
17:00‑17:30 (Suite 2928)
Final Remarks |
17:00‑17:30 (Suite 3028)
Elvira Albert
, Puri Arenas
and German Puebla
Some Issues on Incremental Abstraction-Carrying Code
|
17:20‑18:00 (Suite 3002)
Panel: J. Franco, V. Marek, D. Mitchell, I. Niemela, E. Ternovska (Chair)
|
| |
|
|
|
|
17:30‑17:45 (Suite 3028)
Alexander Serebrenik
and Wim Vanhoof
Fingerprinting Logic Programs
|
| |
18:00‑18:30 (Willow A)
Open-Space, Report back
|
|
|
18:00‑18:30 (Suite 3028)
Siddharth Chitnis, Madhu Yennamani and Gopal Gupta
ExSched: Solving Constraint Satisfaction Problems with the Spreadsheet Paradigm
|
| |
18:30‑19:00 (Suite 3028)
Kim Henriksen
and John Gallagher
A Web-based Tool Combining Different Type Analyses
|
|
19:00‑21:00 (Grand Ballroom A/B)
CAV-ICLP-IJCAR Joint Reception |
19:00‑21:00 (Grand Ballroom A/B)
CAV-ICLP-IJCAR Joint Reception |
19:00‑21:00 (Grand Ballroom A/B)
CAV-ICLP-IJCAR Joint Reception |
|
