20.142 new publication on computer-aided verification

               Humanist Discussion Group, Vol. 20, No. 142.
       Centre for Computing in the Humanities, King's College London
  www.kcl.ac.uk/schools/humanities/cch/research/publications/humanist.html
                        www.princeton.edu/humanist/
                     Submit to: humanist_at_princeton.edu

         Date: Tue, 08 Aug 2006 06:47:24 +0100
         From: Willard McCarty <willard.mccarty_at_kcl.ac.uk>
         Subject: new publication: Computer Aided Verification (LNCS 4144/2006)

[Many of the following seem from the titles to be
rather specialized articles, but at least the
invited talk by Tony Hoare should be of wide interest. --WM]

Volume 4144/2006 (Computer Aided Verification) of
Lecture Notes in Computer Science is now
available on the springerlink.metapress.com web
site at http://springerlink.metapress.com.

Formal Specifications on Industrial-Strength Code
-- From Myth to Reality: (Invited Talk) p. 1
Manuvir Das
DOI: 10.1007/11817963_1

I Think I Voted: E-Voting vs. Democracy: (FLoC Plenary Talk) p. 2
David Dill
DOI: 10.1007/11817963_2

Playing with Verification, Planning and Aspects:
Unusual Methods for Running Scenario-Based
Programs: (Abstract of FLoC Keynote Talk) p. 3
David Harel
DOI: 10.1007/11817963_3

The Ideal of Verified Software: (Invited Talk) p. 5
Tony Hoare
DOI: 10.1007/11817963_4

Antichains: A New Algorithm for Checking
Universality of Finite Automata p. 17
M. De Wulf, L. Doyen, T. A. Henzinger, J. -F. Raskin
DOI: 10.1007/11817963_5

Safraless Compositional Synthesis p. 31
Orna Kupferman, Nir Piterman, Moshe Y. Vardi
DOI: 10.1007/11817963_6

Minimizing Generalized Büchi Automata p. 45
Sudeep Juvekar, Nir Piterman
DOI: 10.1007/11817963_7

Ticc : A Tool for Interface Compatibility and Composition p. 59
B. Thomas Adler, Luca de Alfaro, Leandro Dias Da
Silva, Marco Faella, Axel Legay, Vishwanath Raman, Pritam Roy
DOI: 10.1007/11817963_8

FAST Extended Release: (Tool Paper) p. 63
Sébastien Bardin, Jérôme Leroux, Gérald Point
DOI: 10.1007/11817963_9

Don’t Care Words with an Application to the
Automata-Based Approach for Real Addition: (Extended Abstract) p. 67
Jochen Eisinger, Felix Klaedtke
DOI: 10.1007/11817963_10

A Fast Linear-Arithmetic Solver for DPLL(T) p. 81
Bruno Dutertre, Leonardo de Moura
DOI: 10.1007/11817963_11

Bounded Model Checking for Weak Alternating Büchi Automata p. 95
Keijo Heljanko, Tommi Junttila, Misa Keinänen, Martin Lange, Timo Latvala
DOI: 10.1007/11817963_12

Deriving Small Unsatisfiable Cores with Dominators p. 109
Roman Gershman, Maya Koifman, Ofer Strichman
DOI: 10.1007/11817963_13

Lazy Abstraction with Interpolants p. 123
Kenneth L. McMillan
DOI: 10.1007/11817963_14

Using Statically Computed Invariants Inside the
Predicate Abstraction and Refinement Loop p. 137
Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang
DOI: 10.1007/11817963_15

Counterexamples with Loops for Predicate Abstraction p. 152
Daniel Kroening, Georg Weissenbacher
DOI: 10.1007/11817963_16

cascade: C Assertion Checker and Deductive Engine: (Tool Paper) p. 166
Nikhil Sethi, Clark Barrett
DOI: 10.1007/11817963_17

Yasm : A Software Model-Checker for Verification
and Refutation: (Tool Paper) p. 170
Arie Gurfinkel, Ou Wei, Marsha Chechik
DOI: 10.1007/11817963_18

SAT-Based Assistance in Abstraction Refinement
for Symbolic Trajectory Evaluation p. 175
Jan-Willem Roorda, Koen Claessen
DOI: 10.1007/11817963_19

Automatic Refinement and Vacuity Detection for
Symbolic Trajectory Evaluation p. 190
Rachel Tzoref, Orna Grumberg
DOI: 10.1007/11817963_20

Some Complexity Results for SystemVerilog Assertions p. 205
Doron Bustan, John Havlicek
DOI: 10.1007/11817963_21

Check It Out: On the Efficient Formal
Verification of Live Sequence Charts p. 219
Jochen Klose, Tobe Toben, Bernd Westphal, Hartmut Wittke
DOI: 10.1007/11817963_22

Symmetry Reduction for Probabilistic Model Checking p. 234
Marta Kwiatkowska, Gethin Norman, David Parker
DOI: 10.1007/11817963_23

Communicating Timed Automata: The More
Synchronous, the More Difficult to Verify p. 249
Pavel Krcal, Wang Yi
DOI: 10.1007/11817963_24

Allen Linear (Interval) Temporal Logic –
Translation to LTL and Monitor Synthesis p. 263
Grigore Rosu, Saddek Bensalem
DOI: 10.1007/11817963_25

DiVinE – A Tool for Distributed Verification: (Tool Paper) p. 278
Jirí Barnat, Luboš Brim, Ivana Cerná, Pavel
Moravec, Petr Rockai, Pavel Šimecek
DOI: 10.1007/11817963_26

EverLost: A Flexible Platform for
Industrial-Strength Abstraction-Guided Simulation: (Tool Paper) p. 282
Flavio M. de Paula, Alan J. Hu
DOI: 10.1007/11817963_27

Symbolic Model Checking of Concurrent Programs
Using Partial Orders and On-the-Fly Transactions p. 286
Vineet Kahlon, Aarti Gupta, Nishant Sinha
DOI: 10.1007/11817963_28

Model Checking Multithreaded Programs with Asynchronous Atomic Methods p. 300
Koushik Sen, Mahesh Viswanathan
DOI: 10.1007/11817963_29

Causal Atomicity p. 315
Azadeh Farzan, P. Madhusudan
DOI: 10.1007/11817963_30

Languages of Nested Trees p. 329
Rajeev Alur, Swarat Chaudhuri, P. Madhusudan
DOI: 10.1007/11817963_31

Improving Pushdown System Model Checking p. 343
Akash Lal, Thomas Reps
DOI: 10.1007/11817963_32

Repair of Boolean Programs with an Application to C p. 358
Andreas Griesmayer, Roderick Bloem, Byron Cook
DOI: 10.1007/11817963_33

Termination of Integer Linear Programs p. 372
Mark Braverman
DOI: 10.1007/11817963_34

Automatic Termination Proofs for Programs with Shape-Shifting Heaps p. 386
Josh Berdine, Byron Cook, Dino Distefano, Peter W. O’Hearn
DOI: 10.1007/11817963_35

Termination Analysis with Calling Context Graphs p. 401
Panagiotis Manolios, Daron Vroon
DOI: 10.1007/11817963_36

Terminator : Beyond Safety: (Tool Paper) p. 415
Byron Cook, Andreas Podelski, Andrey Rybalchenko
DOI: 10.1007/11817963_37

CUTE and jCUTE: Concolic Unit Testing and
Explicit Path Model-Checking Tools: (Tool Paper) p. 419
Koushik Sen, Gul Agha
DOI: 10.1007/11817963_38

SMT Techniques for Fast Predicate Abstraction p. 424
Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras
DOI: 10.1007/11817963_39

The Power of Hybrid Acceleration p. 438
Bernard Boigelot, Frédéric Herbreteau
DOI: 10.1007/11817963_40

Lookahead Widening p. 452
Denis Gopan, Thomas Reps
DOI: 10.1007/11817963_41

The Heuristic Theorem Prover: Yet Another SMT
Modulo Theorem Prover: (Tool Paper) p. 467
Kenneth Roe
DOI: 10.1007/11817963_42

LEVER: A Tool for Learning Based Verification: (Tool Paper) p. 471
Abhay Vardhan, Mahesh Viswanathan
DOI: 10.1007/11817963_43

Formal Verification of a Lazy Concurrent List-Based Set Algorithm p. 475
Robert Colvin, Lindsay Groves, Victor Luchangco, Mark Moir
DOI: 10.1007/11817963_44

Bounded Model Checking of Concurrent Data Types
on Relaxed Memory Models: A Case Study p. 489
Sebastian Burckhardt, Rajeev Alur, Milo M. K. Martin
DOI: 10.1007/11817963_45

Fast and Generalized Polynomial Time Memory Consistency Verification p. 503
Amitabha Roy, Stephan Zeisset, Charles J. Fleckenstein, John C. Huang
DOI: 10.1007/11817963_46

Programs with Lists Are Counter Automata p. 517
Ahmed Bouajjani, Marius Bozga, Peter Habermehl,
Radu Iosif, Pierre Moro, Tomáš Vojnar
DOI: 10.1007/11817963_47

Lazy Shape Analysis p. 532
Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz
DOI: 10.1007/11817963_48

Abstraction for Shape Analysis with Fast and Precise Transformers p. 547
Tal Lev-Ami, Neil Immerman, Mooly Sagiv
DOI: 10.1007/11817963_49

Dr Willard McCarty | Reader in Humanities
Computing | Centre for Computing in the
Humanities | King's College London | Kay House, 7
Arundel Street | London WC2R 3DX | U.K. | +44
(0)20 7848-2784 fax: -2980 ||
willard.mccarty_at_kcl.ac.uk www.kcl.ac.uk/humanities/cch/wlm/
Received on Tue Aug 08 2006 - 02:13:11 EDT