|
ACL
|
BMC
|
FATES-RV
|
FCS-ARSPA
|
HOR
|
LICS
|
LSB
|
SAT
|
VERIFY
|
WST
|
| |
08:50‑09:00 (Suite 3102)
Pete Manolios and Matt Wilding |
|
|
|
|
|
|
|
|
08:50‑09:00 (Suite 2628)
Welcome to WST 2006 |
09:00‑09:30 (Suite 3102)
Lee Pike
, Mark Shields
and John Mattews
A Verifying Core for a Cryptographic Language Compiler
|
09:00‑09:20 (Metropolitan B)
Carsten Sinz
SAT-Race
|
09:00‑10:00 (Suite 2828)
Wolfgang Grieskamp
Multi-Paradigmatic Model-Based Testing [ppt]
|
09:00‑10:00 (Metropolitan A)
Andy Gordon
Provable Implementations of Security Protocols [ppt]
|
09:00‑10:00 (Suite 3002)
Eelco Visser
Dynamic rewrite rules [pdf]
|
09:00‑10:00 (Metropolitan A)
Andy Gordon
Provable Implementations of Security Protocols [ppt]
|
09:00‑09:50 (Suite 3228)
Anne Condon
DNA and RNA Molecules: Glimpses Through an Algorithmic Lens
|
09:00‑09:20 (Metropolitan B)
Carsten Sinz
SAT-Race
|
09:00‑10:00 (Suite 3128)
John Rushby
Threatened by a Great Opportunity: Disruptive Innovation in Formal Verification [pdf]
|
09:00‑10:00 (Suite 2628)
Byron Cook
Program termination analyses for free! [ppt]
|
09:20‑09:40 (Metropolitan B)
Olivier Roussel
Pseudo Boolean Evaluation
|
09:20‑09:40 (Metropolitan B)
Olivier Roussel
Pseudo Boolean Evaluation
|
09:30‑10:00 (Suite 3102)
David Hardin, Eric Smith and William Young
A Robust Machine Code Proof Framework for Highly Secure Applications
|
09:40‑10:00 (Metropolitan B)
Armando Tacchella
QBF Evaluation
|
09:40‑10:00 (Metropolitan B)
Armando Tacchella
QBF Evaluation
|
| |
10:00‑10:30
Break |
10:30‑11:00 (Suite 3102)
John Cowles
and Ruben Gamboa
Unique Factorization in ACL2: Euclidean Domains
|
10:30‑11:30 (Suite 2928)
Ilkka Niemela
Bounded Model Checking, Answer Set Programming, and Fixed Points [pdf]
|
10:30‑11:00 (Suite 2828)
Lars Frantzen
, Jan Tretmans and Tim Willemse
A Symbolic Framework for Model-Based Testing
|
10:30‑11:00 (Cirrus)
Long Nguyen
and Bill Roscoe
Efficient group authentication protocols based on human interaction
|
10:30‑11:00 (Suite 3002)
Thomas Ehrhard and Olivier Laurent
Embedding the finitary Pi-calculus in differential interaction nets
|
10:30‑11:00 (Metropolitan A)
Tomas Brazdil, Vaclav Brozek, Vojtech Forejt and Antonin Kucera
Stochastic Games with Branching-Time Winning Objectives
|
10:30‑11:30 (Suite 3228)
Larry Ruzzo
Searching for Noncoding RNA [pdf]
|
10:30‑11:00 (Metropolitan B)
Hans Kleine Büning
and Xishun Zhao
Minimal False Quantified Boolean Formulas
|
10:30‑11:00 (Suite 3128)
Myla Archer and Elizabeth Leonard
Establishing High Confidence in Code Implementations of Algorithms using Formal Verification of Pseudocode
|
10:30‑11:00 (Suite 2628)
Peter Schneider-Kamp
, Juergen Giesl
, Alexander Serebrenik
and Rene Thiemann
Termination Analysis for Logic Programs by Term Rewriting Revisited
|
11:00‑11:30 (Suite 3102)
David Greve
Generalized Congruences in ACL2
|
11:00‑11:30 (Suite 2828)
Jean-Claude Fernandez
, Laurent Mounier
and Jean-luc Richier
A Test Calculus Framework Applied to Network Security Policies
|
11:00‑11:30 (Cirrus)
Jonathan Millen, Joshua Guttman
, John Ramsdell, Justin Sheehy and Brian Sniffen
Call by Contract for Cryptographic Protocols
|
11:00‑11:30 (Suite 3002)
Caroline Priou
Non-deterministic Bohm trees
|
11:00‑11:30 (Metropolitan A)
Dexter Kozen
Coinductive Proof Principles for Stochastic Processes
|
11:00‑11:30 (Metropolitan B)
Horst Samulowitz
and Fahiem Bacchus
Binary Clause Reasoning in QBF
|
11:00‑11:30 (Suite 3128)
Robert Palmer
, Ganesh Gopalakrishnan
and Mike Kirby
Formal Specification and Verification Using +CAL: An Experience Report
|
11:00‑11:30 (Suite 2628)
Manh Thang Nguyen, Maurice Bruynooghe, Danny De Schreye and Michael Leuschel
Program Specialisation as a Pre-processing Step for Termination Analysis
|
11:30‑11:45 (Suite 3102)
Sol Swords and William R. Cook
Soundness of the Simply Typed Lambda Calculus in ACL2
|
11:30‑12:00 (Suite 2928)
Joao Marques-Silva
Interpolant Learning and Reuse in SAT-Based Model Checking
|
11:30‑12:00 (Suite 2828)
Michiel van Osch
Hybrid Input-output Conformance and Test Generation
|
11:30‑12:00 (Cirrus)
Aybek Mukhamedov and Mark Ryan
On Asynchronous Multi-party Contract-Signing
|
11:30‑12:00 (Suite 3002)
Barry Jay
Typing the pattern calculus
|
11:30‑12:00 (Metropolitan A)
Patricia Bouyer
, Thomas Brihaye and Fabrice Chevalier
Control in o-minimal hybrid systems
|
11:30‑12:15 (Suite 3228)
Rajeev Alur
Hybrid Systems Modeling for Regulatory Pathways [ppt]
|
11:30‑12:00 (Metropolitan B)
Daijue Tang and Sharad Malik
Solving Quantified Boolean Formulas with Circuit Observability Don't Cares
|
11:30‑12:00 (Suite 3128)
Bernhard Beckert
and Vladimir Klebanov
Must Program Verification Systems and Calculi be Verified?
|
11:30‑12:00 (Suite 2628)
Naoki Nishida
and Koichi Miura
Dependency Graph Method for Proving Termination of Narrowing
|
11:45‑12:30 (Suite 3102)
"Matt Kaufmann, J Strother Moore
An Overview of Recent and Upcoming ACL2 Developments
|
12:00‑12:30 (Suite 2928)
Toni Jussila and Armin Biere
Compressing BMC Encodings with QBF
|
12:00‑12:30 (Suite 2828)
Juhan P. Ernits
, Andres Kull, Kullo Raiend and Jüri Vain
Generating Tests from EFSM Models using Guided Model Checking and Iterated Search Refinement
|
12:00‑12:30 (Cirrus)
Romain Janvier, Yassine Lakhnech
and Laurent Mazaré
Relating the Symbolic and Computational Models of Security Protocols Using Hashes
|
|
12:00‑12:10 (Metropolitan A)
Murray Patterson
, Yongmei Liu, Eugenia Ternovska and Arvind Gupta
Grounding for Model Expansion in k-Guarded Formulas
|
12:00‑12:30 (Metropolitan B)
Ashish Sabharwal
, Carlos Ansotegui, Carla P. Gomes
, Justin W. Hart
and Bart Selman
QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency
|
|
12:00‑12:30 (Suite 2628)
Yi Wang and Masahiko Sakai
On Non-looping Term Rewriting
|
12:10‑12:20 (Metropolitan A)
Jørgen Villadsen
Nominalization in Intensional Type Theory
|
| |
12:20‑12:30 (Metropolitan A)
Leona F. Fass
A Logical Look at Agents’ Problem-Solving on the Semantic Web
|
12:30‑14:00
Lunch break |
14:00‑14:30 (Willow A)
Mike Gordon, Warren A. Hunt, Jr.
, Matt Kaufmann
and James Reynolds
An Embedding of the ACL2 Logic in HOL
|
14:00‑15:00 (Suite 2928)
Fabio Somenzi
Techniques for proving properties with SAT-based MC [pdf]
|
14:00‑14:30 (Suite 2828)
Cheng Li
and zhe dang
Decompositional Algorithms for Safety Verification and Testing of Aspect-Oriented Systems
|
14:00‑14:30 (Cirrus)
Johannes Borgström, Simon Kramer and Uwe Nestmann
Calculus of Cryptographic Communication
|
14:00‑14:30 (Suite 3002)
Barry Jay
Quantifying the benefits of sub-typing
|
14:00‑14:30 (Metropolitan A)
Thomas Ball
and Orna Kupferman
An Abstraction-Refinement Framework for Multi-Agent Systems
|
14:00‑14:45 (Suite 3228)
Ilya Shmulevich
Insights from Boolean Modeling of Genetic Regulatory Networks [ppt]
|
14:00‑14:30 (Metropolitan B)
Naomi Nishimura
, Prabhakar Ragde
and Stefan Szeider
Solving #SAT using Vertex Covers
|
14:00‑14:30 (Suite 3128)
Sara Van Langenhove
and Albert Hoogewijs
Verifying Sliced Hierarchical Statecharts with SVtL
|
14:00‑14:30 (Suite 2628)
Frederic Blanqui
Higher-order dependency pairs
|
14:30‑15:00 (Willow A)
Julien Schmaltz and Dominique Borrione
Towards a Formal Theory of On Chip Communications in the ACL2 Logic
|
14:30‑15:00 (Suite 2828)
Pieter Koopman, Rinus Plasmeijer and Peter Achten
Model-Based Testing of Thin-Client Web Applications
|
14:30‑15:00 (Cirrus)
Prateek Gupta and Vitaly Shmatikov
Key confirmation and adaptive corruptions in the protocol security logic
|
14:30‑15:00 (Suite 3002)
Nao Hirokawa and Aart Middeldorp
Uncurrying for termination
|
14:30‑15:00 (Metropolitan A)
Daniele Varacca
and Hagen Voelzer
Temporal logics and model checking for fairly correct systems
|
14:30‑15:00 (Metropolitan B)
António Morgado, Paulo Matos
, Vasco Manquinho and Joao Marques-Silva
Counting Models in Integer Domains
|
14:30‑15:00 (Suite 3128)
Laura Ildiko Kovacs
and Tudor Jebelean
Finding Polynomial Invariants for Imperative Loops in the Theorema System
|
14:30‑15:00 (Suite 2628)
Wojciech Moczydlowski
Normalization of intuitionistic set theories
|
14:45‑15:30 (Suite 3228)
Ashish Tiwari
Symbolic Systems Biology: Hybrid Modeling and Analysis of Biological Networks [pdf]
|
15:00‑15:15 (Willow A)
Jared Davis
Memories: Array-like Records for ACL2
|
15:00‑15:30 (Suite 2928)
Erika Abraham
, Bernd Becker
and Marc Herbstritt
Bounded Model Checking with Parametric Data Structures
|
15:00‑15:30 (Suite 2828)
Manoranjan Satpathy
, Qaiser Malik and Johan Lilius
Synthesis of Scenario Based Test Cases from B Models
|
15:00‑15:30 (Cirrus)
Philippe Balbiani
, Yannick Chevalier
and mounira kourjieh
Reasoning about Actions and Obligations
|
15:00‑15:30 (Suite 3002)
Shane O'Conchuir
Proving PSN by simulating non-cal substitution with local substitution
|
15:00‑15:30 (Metropolitan A)
Sharon Shoham
and Orna Grumberg
3-Valued Abstraction: More Precision at Less Cost
|
15:00‑15:15 (Metropolitan B)
Marc Thurley
sharpSAT - counting models with advanced component caching and implicit BCP
|
15:00‑15:30 (Suite 3128)
Achim D. Brucker
and Burkhart Wolff
A Package for Extensible Object-Oriented Data Models with an Application to IMP++
|
15:00‑15:30 (Suite 2628)
Claude Marche and Hans Zantema
Report on termination competition 2006
|
15:15‑15:30 (Willow A)
Matt Kaufmann, J Strother Moore
ACM Software System Award Remarks
|
15:15‑15:30 (Metropolitan B)
Antti Eero Johannes Hyvärinen, Tommi Junttila and Ilkka Niemelä
A Distribution Method for Solving SAT in Grids
|
15:30‑16:00
Break |
16:00‑16:45 (Willow A)
Tony Hoare
The Ideal of Verified Software
|
16:00‑16:30 (Suite 2928)
Xuandong Li
, Sumit Kumar Jha
and Lei Bu
Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming
|
16:00‑17:30 (Suite 2828)
Session 4: Tool Demos |
16:00‑16:30 (Cirrus)
Matthias Anlauff, Dusko Pavlovic, Richard Waldinger and Stephen Westfold
Proving Authentication Properties in the Protocol Derivation Assistant
|
16:00‑17:00 (Suite 3002)
Hugo Herbelin
The duality of computation [pdf]
|
16:00‑16:30 (Metropolitan A)
Anuj Dawar, Martin Grohe, Stephan Kreutzer and Nicole Schweikardt
Approximation Schemes for First-Order Definable Optimization Problems
|
16:00‑17:00 (Suite 3228)
Carolyn Talcott
Pathway Logic: A Logical Approach to Modeling Cellular Processes [pdf]
|
16:00‑18:00 (Metropolitan B)
Poster Session |
16:00‑16:30 (Suite 3128)
Raghavendra Kagalavadi Ramesh
and Deepak D'Souza
Checking Unwinding Conditions for Finite State Systems
|
16:00‑16:30 (Suite 2628)
Joerg Endrullis
, Dieter Hofbauer
and Johannes Waldmann
Decomposing Terminating Rewrite Relations
|
16:30‑17:00 (Suite 2928)
Paul Jackson
and Daniel Sheridan
A compact linear translation for bounded model checking
|
16:30‑17:00 (Cirrus)
DongGook Park
, Colin Boyd
, Byoungcheon Lee and Hwankoo Kim
Responsibility and Credit: New Members of the Authentication Family?
|
16:30‑17:00 (Metropolitan A)
Eldar Fischer
, Frederic Magniez
and Michel de Rougemont
Approximate Satisfiability and Equivalence
|
16:30‑17:00 (Suite 3128)
Dieter Hutter
Automating Proofs of Unwinding Conditions
|
16:30‑17:00 (Suite 2628)
Hans Zantema
Termination of Extended String Rewriting
|
16:45‑18:15 (Willow A)
David Hardin, Tony Hoare, Gerard Holzmann, J Strother Moore, ...
Panel
|
| |
|
|
17:00‑17:10 (Metropolitan A)
Julian Zinn and Rakesh Verma
A Polynomial-time Algorithm for Uniqueness of Normal Forms of Linear Shallow Term Rewrite Systems
|
17:00‑17:45 (Suite 3228)
William Noble
Two Bioinformatics Applications of Dynamic Bayesian Networks [ppt]
|
|
17:00‑18:00 (Suite 2628)
Business Meeting |
17:10‑17:20 (Metropolitan A)
Aaron Hunter
Non-Closure Results for First-Order Spectra
|
17:20‑17:30 (Metropolitan A)
Detlef Kaehler, Ralf Kuesters
and Thomas Wilke
A Dolev-Yao-based Definition of Abuse-free Protocols
|
| |
17:30‑17:40 (Metropolitan A)
Guillaume Burel
and Claude Kirchner
An Abstract Completion Procedure for Cut Elimination in Deduction Modulo
|
| |
| |
| |
|
| |
19:00‑21:30 (outside hotel)
Workshop Dinner |
