ADVANCE PROGRAM

 June 30

Workshop on Implicit Computational Complexity 

A Tutorial Workshop on Realizability Semantics and Applications 

Workshop on Gröbner Bases and Rewriting Techniques

Plenary Invited Speakers Session 

13:40 Dynamic Reachability  
           Neil Immerman (U. Mass) 
14:40 Complexity in AI and Knowledge Representation 
           Christos Papadimitriou (UC Berkeley) 
16:00 The Linear Order in Descriptive Complexity          
         Theory 
           Thomas Schwentick (U. Mainz) 
17:00 Topological Queries in Spatial Databases  
           Victor Vianu (UC San Diego) 
 

July 1

Workshop on Implicit Computational Complexity 

A Tutorial Workshop on Realizability Semantics and Applications 

Workshop on Finite Model Theory and Applications 
 

July 2

LICS

RTA

Solved forms for path ordering constraints 
R. Nieuwenhuis, J.M. Rivero (UPC Barcelona,Spain) 

Jeopardy  
N. Dershowitz (Tel-Aviv Univ), S. Mitra (Bangalore)

 Two-Variable Descriptions of Regularity  
Erich Graedel,  Eric Rosen (RWTH Aachen)

The Two-Variable Guarded Fragment with Transitive Relations  
Harald Ganzinger, Christoph Meyer, Margus Veanes 
(Max-Planck Institut fur Informatik) 

Logics with Aggregate Operators 
Lauri Hella (Univ. of Helsinki), Leonid Libkin (Bell Labs), 
Juha Nurmonen (Univ. of Leicester), Limsoon Wong (KRDL) 

Guarded Fixed Point Logic 
Erich Graedel (RWTH Aachen), 
Igor Walukiewicz (Warsaw Univ.)

On the strong normalization of natural deduction 
P. de Groote (INRIA Lorraine) 

Normalisation in weakly orthogonal rewriting 
V. van Oostrom (Univ. Utrecht) 

Strong normalization of proof-nets modulo 
structural congruences 
R. Di Cosmo (DMI-LIENS), 
S. Guerrini (Queen Mary and Westfield College) 
(talks end at 12:30)

Towards a theory of bisimulation for local names 
Alan Jeffrey (DePaul Univ.), 
Julian Rathke (University of Sussex) 

Weak Bisimulation and Open Maps 
Marcelo Fiore (University of Sussex) 
Gian Luca Cattani (University of Cambridge) 
Glynn Winskel (University of Aarhus) 

Elementary Axioms for Categories of Classes 
Alex K. Simpson (Univ. Edingburgh)

INVITED TALK 
Hierarchical graph decompositions defined by 
grammars and logical formulas 
B. Courcelle (Univ. Bordeaux)

Region analysis and the polymorphic lambda calculus 
Anindya  Banerjee (Stevens Inst. of Technology), 
Nevin Heintze, Jon Riecke (Bell Labs) 

Pattern Matching as Cut Elimination 
Serenella Cerrito, Delia Kesner (Univ. Paris-Sud) 

BREAK (16:35-16:55) 

Some Computational Properties of Intersection Types 
A.Bucciarelli, S.De Lorenzis, 
A.Piperno, I.Salvo (La Sapienza, Roma) 

Type Inference for Recursive Definitions 
Assaf J. Kfoury,  Santiago Pericas (Boston Univ.) 
 
 

Undecidability of the exists-forall part of the  
theory of ground term algebra modulo an AC symbol 
J. Marcinkowski (Univ. Wroclaw) 

Solving one step rewriting formulae 
A-C. Caron, F. Seynhaeve, S. Tison, 
M. Tommasi (Univ. Lille) 

A new result about the decidability of the 
existential one-step rewriting theory 
S. Limet, P. Rety (Univ. Orleans) 
(last talk ends 17:15) 

RTA BUSINESS MEETING (starts 17:30) 

July 3

  LICS

RTA

A fully syntactic AC-RPO 
A. Rubio (Univ. Catalunya) 
 
Theory path orderings 
J. Stuber (MPI, Saarbruecken)

Subtyping Recursive Types in Kernel Fun 
Dario Colazzo, Giorgio Ghelli (Univ. Pisa)

A Fragment Calculus - towards a model of  
Separate  Compilation, Linking and Binary Compatibility 
Sophia Drossopoulou,  Susan Eisenbach, 
David Wragg (Imperial College) 

Proof techniques for Cryptographic Processes 
Michele Boreale (La Sapienza), 
Rocco De Nicola, Rosario Pugliese (Univ. di Firenze) 

On Hoare Logic and Kleene Algebra with Tests 
Dexter Kozen (Cornell Univ)

Deciding the word problem in the union of  
equational theories sharing constructors  
F. Baader (RWTH Aachen), 
 C. Tinelli (Univ. Illinois at Urbana-Champaign) 

Normalization via rewrite closure  
L. Bachmair, C. Ramakrishnan, 
I.V. Ramakrishnan, A. Tiwari (SUNY Stony Brook) 

Test sets for the universal and existential closure  
of regular tree languages  
D. Hofbauer (TU Berlin), 
M. Huber (Univ. Kassel) 
(talks end at 12:30)

Full Abstraction via Realisability 
Michael Marz, Alexander  Rohr, 
Thomas Streicher (TU Darmastadt) 

On Bunched Predicate Logic 
David J. Pym (Queen Mary and Westfield College, London) 

Abstract Syntax and Variable Binding 
Marcelo Fiore (Univ. of Sussex), 
Gordon  Plotkin, Daniele Turi (Univ. of Edinburgh) 
 

INVITED TUTORIAL 
Higher Order Rewriting 
F. van Raamsdonk (CWI)

Semantical analysis of higher-order abstract syntax 
Martin  Hofmann (Edinburgh Univ) 

A New Approach to Abstract Syntax Involving Binders 
M.J. Gabbay, A.M. Pitts (Cambridge Univ) 

BREAK (16:35-16:55) 

Paramodulation with Non-Monotonic Orderings 
Miquel Bofill,  Guillem Godoy,  Robert Nieuwenhuis, 
Albert Rubio (Technical  University of Catalonia) 

Full completeness of the multiplicative linear logic  
of Chu  spaces 
Harish Devarajan (Stanford Univ.), 
Dominic Hughes (Stanford Univ.), 
Gordon Plotkin (Edinburgh Univ.), 
Vaughan Pratt (Stanford Univ.) 

18:00 LICS BUSINESS MEETING

The Maude system 
M. Clavel, F. Duran, S. Eker, 
P. Lincoln, N. Marti-Oliet, 
J. Meseguer, J.F. Quesada (SRI) 

TOY: A Multiparadigm Declarative System 
F.J. Lopez-Fraguas, 
J. Sanchez-Hernandez (UCM, Madrid) 

BREAK (16:25-16:35) 

UniMoK: A System for Combining Equational  
Unification Algorithms 
S. Kepser, J. Richts (Univ. Munich) 

LRR: A Laboratory for Rapid Term  
Graph Rewriting 
R. Verma, S. Senanayake (Univ. Houston)

July 4

LICS

RTA

Decidability for Left-Linear Growing TRS 
T. Nagaya, Y. Toyama (JAIST, Japan) 

Transforming Context-Sensitive Rewrite Systems 
 J. Giesl (Darmstadt Univ), 
 A. Middeldorp (Univ. Tsukuba)

Weak Bounded Arithmetic, the Diffie-Hellman  
Problem and  Constable's Class K 
Jan Johannsen (UCSD) 
 

First-Order Logic vs. Fixed-Point Logic in  
Finite Set  Theory 
Albert Atserias, Phokion G. Kolaitis (UCSC) 

Entailment of Atomic Set Constraints is  
PSPACE-Complete 
Joachim Niehren,, Martin Mueller (Univ. Saarlandes), 
Jean-Marc Talbot (Max-Planck Institut fur Informatik) 

A Superposition Decision Procedure for the  
Guarded Fragment  with Equality 
Harald Ganzinger (Max-Planck Institut fur Informatik), 
Hans de Nivelle (U. Amsterdam)

The calculus of algebraic constructions 
F. Blanqui, J.-P. Jouannaud, (Univ. Paris-Sud), 
M. Okada (Keio Univ.) 

HOL-lambdasigma 
G. Dowek (INRIA),  T. Hardin (LIP6), 
C. Kirchner  (LORIA & INRIA) 

Session ends at 12:00

Working with arms: complexity results on atomic  
representations of Herbrand models 
Georg Gottlob, Reinhard Pichler (TU Wien) 

Logics with Counting, Auxiliary Relations, and  
Lower Bounds  for Invariant Queries 
Leonid Libkin (Bell Labs) 

Counting and Addition cannot express  
Deterministic Transitive  Closure 
Matthias Ruhl (MIT)

INVITED TALK 
On the connections between rewriting and 
formal language theory 
F. Otto (Univ. Kassel)

Parametric Quantitative Temporal Reasoning 
E. Allen Emerson, 
Richard J.Trefler (Univ. texas, Austin) 

Modular Temporal Logic 
Augustin Baziramwabo, Pierre McKenzie (Univ. Montreal), 
Denis Therien (McGill Univ.) 

16:35 - 16:55 BREAK 

On the Verification of Broadcast Protocols 
Javier Esparza (TU Munich),  Alain Finkel (ENS Cachan), 
Richard Mayr (TU Munich) 

On the Expressive Power of CTL* 
Faron Moller (Uppsala Univ), 
Alex Rabinovich (Tel Aviv Univ.) 
 

A rewrite system associated with quadratic  
Pisot units 
C. Frougny (Univ. Paris), 
J. Sakarovitch (CNRS, Paris) 

Fast rewriting of symmetric polynomials 
M. Gobel (D.F. Zentrum) 

On Implementation of Tree Synchronized  
Languages 
F. Saubion, I. Stephan (Univ. d'Angers) 

Session ends 17:15 
END OF RTA

JULY 5

LICS

OTHER EVENTS

Proving Security  Protocols Correct 
 L. Paulson (Cambridge Univ.)

Workshop on Explicit Substitutions 
 

Reasoning about common knowledge with  
infinitely many agents 
Joseph Halpern, Richard Shore (Cornell Univ.) 

Workshop on Strategies in Automated Deduction 
 
 

Parikh's Theorem in Commutative Kleene Algebra 
Dexter Kozen (Cornell Univ.), 
Mark W. Hopkins (Adaptive Micro Systems) 

The Higher-order Recursive Path Ordering 
Jean-Pierre Jouannaud (Univ. Paris-Sud), 
Albert Rubio (Tech. Univ. Catalonia) 

Extensional Equality in Intensional Type Theory 
Thorsten Altenkirch (LMU, Munich)

 5th International SPIN Workshop on 
Theoretical Aspects of Model Checking 
 

A fully abstract game semantics for finite nondeterminism 
Russell Harmer (Imperial College), 
Guy McCusker (Univ. Sussex) 

Concurrent Games and Full Completeness 
Samson Abramsky (Edinburgh Univ.) , 
Paul-Andre Mellies (CNRS Paris) 

Non-deterministic Games and Program Analysis: 
An application to security 
Pasquale Malacaria, Chris Hankin (Imperial College) 
 

Workshop on Formal Methods and Security Protocols 
 

Correctness of Multiplicative Proof Nets is Linear 
Stefano Guerrini (Queen Mary and Westfield College) 

Linear types and non-size-increasing  
polynomial time  computation 
Martin Hofmann (Edinburgh Univ.)

Using formal verification methods in an 
industrial environment for a  decade. 
Conclusions and perspectives. 

Gerard Roucairol 
Groupe Bull R&D President 
 

On the meaning of logical rules : ludics 
J.Y. Girard (CNRS, Marseille) 

END OF LICS

July 6

CAV TUTORIAL DAY

OTHER EVENTS

Symbolic model checking 
Edmund Clarke (CMU)

Workshop on Intuitionistic Modal Logics and  
Applications

Hardware Verification 
David Dill (Stanford Univ.)

Workshop on Complexity-Theoretic and  
Recursion-Theoretic Methods in  
Databases andArtificial Intelligence

Specification and verification of timed systems  
Joseph Sifakis (Verimag)

Workshop on Automation of Proof by Mathematical Induction

Model checking of timed and hybrid systems 
Rajeev Alur (UPenn)

Workshop on Symbolic Model Checking 

Workshop on Run-Time Result Verification

Moderator: Alan Bundy 
Panelists: Ruzena Bajcsy and Simon Bensasson

July 7

CAV

CADE

INVITED PAPER 
Stalmarck's method and QBF solving 
Gunnar Stalmarck (Prover Technology)

A dynamic programming approach to  
categorial deduction 
Philippe de Groote (INRIA Lorraine) 

Tractable Transformations from Modal  
Provability Logics into First-Order Logic 
Stephane Demri (Laboratoire LEIBNIZ), 
Rajeev Gore (ANU, Canberra)

Proof of Correctness of a Processor with Reorder  
Buffer using the Completion Functions Approach 
Ravi Hosabettu (Univ. of Utah), Mandayam Srivas (SRI), 
Ganesh Gopalakrishnan (Univ. of Utah) 

Verifying Safety Properties of a PowerPC(TM) 
Microprocessor Using Symbolic Model Checking  
without BDDs 
Armin Biere, Edmund Clarke, 
Richard Raimi, Yunshan Zhu (CMU) 

Model Checking the IBM Gigahertz Processor: An 
Abstraction Algorithm for High-Performance Netlists 
Jason Baumgartner (IBM), Tamir Heyman (IBM), 
Vigyan Singhal (Cadence), Adnan Aziz (U. Texas, Austin) 

Validation of Pipelined Processor Designs using 
Esterel Tools: A Case Study 
S. Ramesh (IIT Bombay), Purandar Bhaduri (Tata Infotech)

INVITED TALK 
Decision procedures for guarded logics 
Erich Graedel (RWTH Aachen) 

A PSPACE Algorithm for Graded Modal Logic 
Stephan Tobies (RWTH Aachen) 

Session ends at 12:00

Automated verification of a parametric real-time  
program: the ABR conformance protocol 
Beatrice Berard, Laurent Fribourg (ENS Cachan) 

Test generation derived from model-checking 
Thierry Jeron, Pierre Morel (IRISA/INRIA) 

Latency Insensitive Protocols 
Luca P. Carloni (Berkeley), 
Kenneth L. McMillan (Cadence), 
Alberto L.  Sangiovanni-Vincentelli (Berkeley)

Solvability of Context Equations with  
Two Context Variables is Decidable 
Manfred Schmidt-Schauss (J.-W.-Goethe-Univ.), 
Klaus U. Schulz (Univ. Munchen) 

Complexity of the higher order matching 
Tomasz Wierzbicki (University of Wroclaw) 

Solving equational problems efficiently 
Reinhard Pichler (TU Wien)

Handling Global Conditions in Parametrized  
System Verification  
Parosh Aziz Abdulla (Uppsala), 
Ahmed Bouajjani (VERIMAG), 
Bengt Jonsson (Uppsala),  Marcus Nilsson (Uppsala) 

Verification of Infinite-State Systems by Combining 
Abstraction and Reachability Analysis 
Parosh Aziz Abdulla (Uppsala), 
Aurore Annichini, Saddek Bensalem, 
Ahmed Bouajjani (VERIMAG), 
Peter Habermehl (LIAFA), 
Yassine Lakhnech (Kiel) 

Experience with Predicate Abstraction 
Satyaki Das, David L. Dill (Stanford Univ.), 
Seungjoon Park (RIACS) 
 

VSDITLU: a verifiable symbolic definite  
integral table look-up 
A. A. Adams, H. Gottliebsen, S. A. Linton, 
U. Martin (University of St Andrews) 

A Framework for the Flexible Integration of a Class of  
Decision Procedures into Theorem Provers 
Predrag Janicic (Univ. Belgrade) 
Alan Bundy, Ian Green (Univ. Edinburgh) 

Presenting Proofs in a Human-Oriented Way 
Helmut Horacek (Univ. des Saarlandes)

July 8 

CAV

CADE

INVITED TALK 
Visual Verification of Parameterized Programs 
Zohar Manna (Stanford Univ.) 
 
 

Model Checking of Safety Properties 
Orna Kupferman (Jerusaalem), 
Moshe Y. Vardi (Rice Univ.) 

A Complete Finite Prefix for Process Algebra 
Rom Langerak, Ed Brinksma (Twente) 

The Mathematical Foundation of Symbolic  
Trajectory Evaluation 
Ching-Tsun Chou (Intel) 

Assume-Guarantee Refinement Between  
Different Time Scales 
Thomas Henzinger, Shaz Qadeer, 
Sriram Rajamani (Berkeley)

On the Universal Theory of Varieties of Distributive  
Lattices with Operators:  
Some Decidability and Complexity Results 
Viorica Sofronie-Stokkermans (MPI Saarbrucken) 

Maslov's Class K Revisited 
Ullrich Hustadt, Renate A. Schmidt (Manchester Univ.) 

Prefixed Resolution - A Resolution Method for  
Modal and Description Logics 
Carlos Areces, Hans de Nivelle, 
Maarten de Rijke (Univ. of Amsterdam) 

Session ends at 12:00

Efficient Decision Prcedures for Model  
Checking of Linear Time Logic Properties 
Roderick Bloem (Colorado), Kavita Ravi (Cadence), 
Fabio Somenzi (Colorado) 

Stutter-invariant Languages, omega-automata, and  
Temporal logic 
Kousha Etessami (Bell Labs) 

Improved Automata Generation for Linear Time 
Temporal Logic 
 Marco Daniele (Rome), Fausto Giunchiglia (Trento), 
Moshe Y. Vardi (Rice Univ.)

Session starts 13:45 

Twelf - A Meta-Logical Framework for Deductive Systems 
Frank Pfenning, Carsten Schurmann (CMU) 

INKA 5.0 - A Logic Voyager 
Serge Autexier (Univ. des Saarlandes), 
Dieter Hutter, Heiko Mantel, Axel Schairer (DFKI) 

CutRes 1.0: Cut Elimination by Resolution 
Matthias Baaz, Alexander Leitsch, Georg Moser (TU Wien) 

MathWeb, an Agent-Based Communication Layer for  
Distributed Automated Theorem Proving 
Andreas Franke, Michael Kohlhase (Univ. des Saarlandes) 

Using OBDDs for the validation of Skolem  
verification conditions 
E. Pascal Gribomont, Nachaat Salloum (Univ. Liege) 

Fault-Tolerant Distributed Theorem Proving 
Jason Hickey (Cornell Univ.) 

Waldmeister - Improvements in Performance and Ease of Use 
Thomas Hillenbrand, Andreas Jaeger, 
Bernd Lochner (Univ. Kaiserslautern)

A Toolbox for the Analysis of Discrete  
Event Dynamic Systems 
Peter Buchholz, Peter Kemper (Dortmund Univ.) 

TIPPtool: Compositional Specification and Analysis 
of Markovian Performance Models 
Holger Hermanns, Vassilis Mertsiotakis, 
Markus Siegle (Erlangen Univ.) 

Java Bytecode Verification by Model-Checking 
David Basin, Stefan Friedrich (Freiburg Univ.), 
Joachim Posegga, Harald Vogt (Deutsche Telekom) 

NuSMV: a new Symbolic Model Verifier 
Alessandro Cimatti (Trento), 
Edmund Clarke (CMU), Fausto Giunchiglia (Trento), 
Marco Roveri (Milano) 

PIL/SETHEO: A Tool for the Automatic Analysis of 
Authentication Protocols 
Johann Schumann (Munchen) 

Session ends 17:15

Formal Metatheory using Implicit Syntax, and an  
Application to Data Abstraction for  
Asynchronous Systems 
Amy P. Felty, Douglas J. Howe (Bell Labs), 
Abhik Roychoudhury (SUNY at Stony Brook) 

A formalization of Static Analyses in System F 
Frederic Prost (ENS-Lyon) 

On explicit reflection in theorem proving and  
formal verification 
Sergei N. Artemov (Cornell Univ.) 
 

18:30-20:30 CADE BUSINESS MEETING 
 

July 9

CAV

CADE

INVITED TALK 
Formal Methods for Conformance Testing:  
Theory can be Practical! 
Ed Brinksma (University of Twente) 
 

Kimba, A Model Generator for Many-Valued  
First-Order Logics 
Karsten Konrad (Univ. des Saarlandes), 
D. A. Wolfram (ANU, Canberra) 

A Compiler and Abstract Machine Based  
Implementation of Lambda Prolog 
Gopalan Nadathur, Dustin J. Mitchell (Univ. of Chicago) 

Vampire 
Alexandre Riazanov, Andrei Voronkov (Uppsala Univ.) 

E 0.3 
Stephan Schulz (TU Munchen) 
 
 

On the Representation of Probabilities over 
Structured Domains 
Marius Bozga, Oded Maler (VERIMAG) 

Model Checking Partial State Spaces with 3-Valued 
Temporal Logics 
Glenn Bruns, Patrice Godefroid (Bell Labs) 

Elementary Microarchitecture Algebra 
John Matthews, John Launchbury (Oregon) 

Verifying sequential consistency on shared memory  
multiprocessor systems  
Thomas A. Henzinger, Shaz Qadeer, 
Sriram K. Rajamani (Berkeley) 
 

INVITED TALK 
Rewrite-based Deduction and Symbolic Constraints 
Robert Nieuwenhuis (UPC Barcelona) 

Towards an Automatic Analysis of Security Protocols in  
First-Order Logic 
Christoph Weidenbach (MPI Saarbrucken)

Optimizing Symbolic Model Checking for  
Invariant-Rich Models  
Bwolen Yang, Reid Simmons, 
Randal E. Bryant, David R. O'Hallaron (CMU) 

Efficient Timed Reachability Analysis using Clock  
Difference Diagrams  
Gerd Behrmann, Kim G. Larsen (BRICS), 
Justin Pearson (Uppsala), Carsten Weise (BRICS), 
Wang Yi (Uppsala) 
 
 

A Confluent Connection Calculus 
Peter Baumgartner (Univ. Koblenz), 
Norbert Eisinger (Univ. Munchen), 
Ulrich Furbach (Univ. Koblenz) 

Abstraction-Based Relevancy Testing for  
Model Elimination 
Marc Fuchs (TU Munchen), Dirk Fuchs (Univ. Kaiserslautern) 

A Breadth-First Strategy for Mating Search 
Matthew Bishop (CMU)

Mechanizing Proofs of Computation Equivalence   
Marcelo Glusman, Shmuel Katz (Technion) 

Linking Theorem Proving and Model-Checking with 
Well-Founded Bisimulation 
Panagiotis Manolios (Univ. Texas Austin), 
Kedar Namjoshi (Bell Labs), 
Robert Sumners (Univ. Texas Austin) 

Automatic verification of combinational and 
pipelined FFT circuits  
Per Bjesse (Chalmers)

CASC-16 Competition of Automated Theorem  
Proving Systems 
Chairs: Geoff Sutcliffe and Christian Suttner

July 10

CAV

CADE

INVITED TALK 
Abstract interpretation applied to the 
verification of Ariane5 software             
Alain Deutsch (Inria)

SPASS Version 1.0.0 
Christoph Weidenbach et al. (MPI Saarbrucken) 

KK: a theorem prover for K 
Andrei Voronkov (Uppsala Univ.) 

An ML Editor Based on Proofs-as-Programs 
Jon Whittle, Alan Bundy, 
Richard Boulton (Univ. of Edinburgh), 
Helen Lowe (Glasgow Caledonian Univ.) 

MCS: Model-based Conjecture Searching 
Jian Zhang (Hong Kong Univ.)

Efficient Analysis of Cyclic Definitions 
Kedar S. Namjoshi, Robert P. Kurshan (Bell Labs) 

A theory of restrictions for logics and automata 
Nils Klarlund (AT&T Labs) 

Model Checking using Automatic Test-Pattern Generation 
Vamsi Boppana, Sreeranga P. Rajan, 
Koichiro Takayama, Masahiro Fujita (Fujitsu Labs) 

Automatic Verification of Abstract State Machines 
Marc Spielmann (RWTH Aachen) 
 

INVITED TALK 
Embedding Programming Languages in Theorem Provers 
Tobias Nipkow (TU Munchen) 

Extensional Higher-Order Paramodulation and  
RUE-Resolution 
Christoph Benzmuller (Univ. des Saarlandes) 

Automatic Generation of Proof Search  
Strategies for Second-order Logic 
Raul H. C. Lopes (Univ. of Leeds) 

END OF CADE

Abstract and Model Check while you Prove 
Hassen Saidi, Natarajan Shankar (SRI) 

Deciding Equality Formulas by  
Small-Domains Instantiations 
A. Pnueli, Y. Rodeh, 
O. Shtrichman, M. Siegel (Weizmann Inst.) 

Exploiting Positive Equality in a Logic of  
Equality with Uninterpreted Functions 
Randal E. Bryant (CMU), Steven German (IBM), 
Miroslav N. Velev (CMU)

END OF CAV

 July 11

Workshop CALCULEMUS: Systems for Integrated  
Computation and Deduction 

Workshop on Formal Methods for Industrial  
Critical Systems 
 

July 12

Workshop CALCULEMUS: Systems for Integrated  
Computation and Deduction 

Workshop on Formal Methods for Industrial  
Critical Systems