Bibliography

ABD⁺00

E. Asarin, O. Bournez, T. Dang, O. Maler, and A. Pnueli.
Effective controller synthesis of switching controllers for linear systems.
Proceedings of the IEEE, 88(7):1011-1025, 2000.

AGP⁺99

K. Altisen, G. Gößler, A. Pnueli, J. Sifakis, and S. Tripakis.
A framework for scheduling as controller synthesis.
In N. Halbwachs and D. Peled, editors, Proc. 11^st Intl. Conference on Computer Aided Verification (CAV'99), volume 1633 of Lect. Notes in Comp. Sci., Springer-Verlag, 1999.
Submitted.

AMP95

E. Asarin, O. Maler, and A. Pnueli.
Symbolic controller synthesis for discrete and timed systems.
In P. Antsaklis, W. Kohn, A. Nerode, and S. Sastry, editors, Hybrid System II, volume 999 of Lect. Notes in Comp. Sci. Springer-Verlag, 1995.

AMP96

R. Alur, K. L. McMillan, and D. Peled.
Model checking of correctness conditions for concurrent objects.
In Proc. 11th IEEE Symp. Logic in Comp. Sci., pages 219-228, 1996.

AMP98

E. Asarin, O. Maler, and A. Pnueli.
On discretization of delays in timed automata and digital circuits.
In R. De Simone and D. Sangiorgi, editors, Proceedings of the 9th International Conference on Concurrency (CONCUR), Lect. Notes in Comp. Sci. Springer-Verlag, 1998.

AMPS98

E. Asarin, O. Maler, A. Pnueli, and J. Sifakis.
Controller synthesis for timed automata.
In IFAC Symposium on System Structure and Control, pages 469-474. Elsevier, 1998.

AP98

T. Arons and A. Pnueli.
Verification of data-insensitive circuits: An in-order-retirement case study.
In G. Gopalakrishnan and P. Windley, editors, Proc. 2nd Intl. Conference on Formal Methods in Computer-Aided Design (FMCAD'98), volume 1522 of Lect. Notes in Comp. Sci., pages 351-368. Springer-Verlag, 1998.

AP99

T. Arons and A. Pnueli.
Verifying tomasulo's algorithm by refinement.
In N. Sherwani and A. Kumar, editors, Twelfth International Conference on VLSI Design, pages 306-309, Goa, India, Jan. 1999.

AP00

T. Arons and A. Pnueli.
A comparison of two verification methods for speculative instruction execution.
In S. Graf and M. Schwartzbach, editors, Proc. 6^th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 487-502. Springer-Verlag, 2000.

AP01

T. Arons and A. Pnueli.
A methodology for deductive verification of out-of-order execution systems based on predicted values.
Technical Report MCS01-04, Weizmann Institute, February 2001.

APR⁺01

T. Arons, A. Pnueli, S. Ruah, J. Xu, and L. Zuck.
Parameterized verification with automatically computed inductive assertions.
In Proc. 13^rd Intl. Conference on Computer Aided Verification (CAV'01), Lect. Notes in Comp. Sci., Springer-Verlag, 2001.
To appear.

Aro01

T. Arons.
Using timstamping and history variables to verify sequential consistency.
In Proc. 13^rd Intl. Conference on Computer Aided Verification (CAV'01), Lect. Notes in Comp. Sci., Springer-Verlag, 2001.
To Appear.

ASBL99

U. Alon, M. G. Surette, N. Barkai, and S. Leibler.
Robustness in bacterial chemotaxis.
Nature, 397:168-171, 1999.

BCCZ99

A. Biere, A. Cimatti, E. Clarke, and Y. Zhu.
Symbolic model checking without BDDs.
In Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS99), Lect. Notes in Comp. Sci. Springer-Verlag, 1999.

BCM⁺92

J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang.
Symbolic model checking: $10\sp{20}$ states and beyond.
Information and Computation, 98(2):142-170, 1992.

BCMD90

J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill.
Sequential circuit verification using symbolic model checking.
Technical report, Carnegie Mellon University, 1990.

BD94

J. R. Burch and D. L. Dill.
Automatic verification of pipelined microprocessor control.
In D. Dill, editor, Proc. 6^th Intl. Conference on Computer Aided Verification (CAV'94), volume 818 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 68-80, 1994.

Bir93

J.C. Birget.
State-complexity of finite-state devices, state compressibility and incompressibility.
Mathematical Systems Theory, 26(3):237-269, 1993.

BK95

D.A. Basin and N. Klarlund.
Hardware verification using 2nd-order logic.
In P. Wolper, editor, Proc. 7^th Intl. Conference on Computer Aided Verification (CAV'95), volume 939 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 31-41, 1995.

BMP99

O. Bournez, O. Maler, and A. Pnueli.
Orthogonal polyhedra: Representation and computation.
In F. Vaandrager and J. van Schuppen, editors, Hybrid Systems: Computation and Control, volume 1569 of Lect. Notes in Comp. Sci., pages 46-60. Springer-Verlag, 1999.

BMSU97

N.S. Bjørner, Z. Manna, H.B. Sipma, and T.E. Uribe.
Deductive verification of real-time systems using STeP.
In 4th Intl. AMAST Workshop on Real-Time Systems, volume 1231 of Lect. Notes in Comp. Sci., pages 22-43. Springer-Verlag, May 1997.

BMT99

M. Bozga, O. Maler, and S. Tripakis.
Efficient verification of timed automata using dense and discrete time semantics.
In L. Pierre and T. Kropf, editors, International Conference on Correct Hardware Design and Verification Methods (CHARME), Lect. Notes in Comp. Sci. Springer-Verlag, 1999.

BOMS⁺00

R. Bar-Or, R. Maya, L.A. Segel, U. Alon, A.J. Levine, and M. Oren.
Generation of oscillations by the p53-mdm2 feedback loop: A theoretical and experimental study.
PNAS, 97(21):11250-11255, 2000.

Bry86

R.E. Bryant.
Graph-based algorithms for Boolean function manipulation.
IEEE Transactions on Computers, C-35(12):1035-1044, 1986.

CHKP01

I.R. Cohen, D. Harel, N. Kam, and A. Pnueli.
T cell activation: Statecharts-based modeling and verification.
Technical report, The Weizmann Institute of Science, Rehovot, Israel, 2001.

Coh00

I.R. Cohen.
Tending Adam's Garden: Evolving the Cognitive Immune Self.
Academic Press, 2000.

DH98

W. Damm and D. Harel.
LSC's: Breathing life into message sequence charts.
Technical Report CS98-09, Weizmann Institute, July 1998.

DH01

W. Damm and D. Harel.
LSCs: Breathing life into message sequence charts.
Formal Methods in System Design, 19(1), 2001.
Preliminary version appeared in Proc. 3rd IFIP Int. Conf. on Formal Methods for Open Object-Based Distributed Systems (FMOODS'99).

DJHP98

W. Damm, B. Josko, H. Hungar, and A. Pnueli.
A compositional real-time semantics of STATEMATE designs.
In W.-P. de Roever, H. Langmacck, and A. Pnueli, editors, Compositionality - the Significant Difference, Proceedings COMPOS'97, volume 1536 of Lect. Notes in Comp. Sci., pages 186-238. Springer-Verlag, 1998.

DP97

W. Damm and A. Pnueli.
Verifying out-of-order executions.
In H.F. Li and D.K. Probst, editors, Advances in Hardware Design and Verification: IFIP WG 10.5 International Conference on Correct Hardware Design and Verification Methods (CHARME), pages 23-47, Montreal, 1997. Chapmann & Hall.

DPR98

W. Damm, A. Pnueli, and S. Ruah.
Herbrand automata for hardware verification.
In R. De Simone and D. Sangiorgi, editors, Proceedings of the 9th International Conference on Concurrency (CONCUR'98), Lect. Notes in Comp. Sci. Springer-Verlag, 1998.

Flo67

R.W. Floyd.
Assigning meanings to programs.
Proc. Symposia in Applied Mathematics, 19:19-32, 1967.

FP01

D. Fisman and A. Pnueli.
Beyond regular model checking.
Technical report, Dept. of Applied Mathematics, Weizmann Institute of Science, 2001.

Ger00

S. German.
Personal Communication, 2000.

GH96

N. Globerman and D. Harel.
Complexity results for two-way and multi-pebble automata and their logics.
Theor. Comp. Sci., 143:161-184, 1996.

GHK00

E. Gery, D. Harel, and H. Kugler.
The Rhapsody Semantics of UML Statecharts.
Technical report, Weizmann Institute, 2000.

GP00

O. Grinchtein and A. Pnueli.
Dense-time analysis with fractional adjustment steps.
Technical report, The John von Neumann Minerva Center, the Weizmann Institute, 2000.

Gwe95

L. Gwennap.
Intel's P6 uses decoupled superscalar design.
Microprocessor Report, 9(2):9-15, 1995.

Har01

D. Harel.
From play-in scenarios to code: An achievable dream.
IEEE Computer, 34(1):53-60, 2001.
Also, Proc. Fundamental Approaches to Software Engineering (FASE), Lecture Notes in Computer Science, Vol. 1783 (Tom Maibaum, ed.), Springer-Verlag.

HG97

D. Harel and E. Gery.
Executable object modeling with statecharts.
Computer, pages 31-42, July 1997.
Also in Proc. 18th Int. Conf. Soft. Eng., Berlin, IEEE Press, March, 1996, pp. 246-257.

HH00

R. Hadany and D. Harel.
A multi-scale method for drawing graphs nicely.
In Proc. 25th Int. Workshop on Graph-Theoretic Concepts in Computer Science (WG'99), volume 1665 of Lect. Notes in Comp. Sci., pages 262-277. Springer-Verlag, 2000.

HHLM99

L.H. Hartwell, J.J. Hopfield, S. Leibler, and A.W. Murray.
From molecular to modular cell biology.
Nature, 402:47-52, 1999.

HJJ⁺95

J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm.
Mona: Monadic second-order logic in practice.
In E. Brinksma, W.R. Cleaveland, W.R., K.G. Larsen, T. Margaria, and B. Steffen, editors, Proc. 1^st Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95), volume 1019 of Lect. Notes in Comp. Sci., Springer-Verlag, 1995.
Also available through http://www.brics.dk/klarlund/Mona/main.html.

HK00a

D. Harel and Y. Koren.
A fast multi-scale method for drawing large graphs.
In Proc. Graph Drawing 2000 (GD 2000), 2000.

HK00b

D. Harel and H. Kugler.
Synthesizing state-based object systems from LSC specifications.
In Proc. 5th Inf. Conf. on Implementation and Application of Automata (CIAA'00), Lect. Notes in Comp. Sci. Springer-Verlag, July 2000.
To appear.

HK00c

D. Harel and O. Kupferman.
On the behavioral inheritance of of state-based objects.
In Proc. 34th Int. Conf. on Components and Object Technology, Santa Barbara, August 2000. IEEE Computer Society.

HN96

D. Harel and A. Naamad.
The STATEMATE semantics of statecharts.
ACM Trans. Software Engin. Methods, 5(4):293-333, 1996.

HY00

D. Harel and G. Yashchin.
Algorithm for blob hierarchy layout.
In Proc. working Conf. on Advanced Visual Interfaces (AVI'2000), pages 29-40. ACM Press, 2000.

KAL99

M. Kaufman, F. Andris, and O. Leo.
A logical analysis of t cell activation and anergy.
PNAS, 96:3894-3899, 1999.

KCH01

N. Kam, I.R. Cohen, and D. Harel.
The immune system as a reactive system: Modeling t cell activation with statecharts.
In Visual Languages and Formal Methods. IEEE, September 2001.

KHCed

N. Kam, D. Harel, and I.R. Cohen.
The immune system as a reactive system: Modeling t cell activation with statecharts.
Bull. Math. Biol., Submitted.

KHP⁺00

H. Kugler, D. Harel, A. Pnueli, Y. Lu, and Y. Bontemps.
Temporal Logic for Live Sequence Charts.
Technical report, Weizmann Institute, 2000.

KKPR99a

Y. Kesten, A. Klein, A. Pnueli, and G. Raanan.
Bridging the E-Business gap through formal verification.
In M.G. Hinchey and J.B. Bowen, editors, Industrial-Strength Formal Methods in Practice, Formal Approaches to Computing and Information Technology series, pages 117-137. Springer-Verlag, 1999.

KKPR99b

Y. Kesten, A. Klein, A. Pnueli, and G. Raanan.
A perfecto verification: Combining model checking with deductive analysis to verify real-life software.
In J.M. Wing, J. Woodcock, and J. Davies, editors, FM'99 - Formal Methods, volume 1708 of Lect. Notes in Comp. Sci., pages 173-194. Springer-Verlag, 1999.

KMM⁺97

Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar.
Symbolic model checking with rich assertional languages.
In O. Grumberg, editor, Proc. 9^th Intl. Conference on Computer Aided Verification, (CAV'97), volume 1254 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 424-435, 1997.

KMM⁺01

Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar.
Symbolic model checking with rich assertional languages.
Theor. Comp. Sci., 256:93-112, 2001.

KMP00

Y. Kesten, Z. Manna, and A. Pnueli.
Verification of clocked and hybrid systems.
Acta Informatica, 36(11):836-912, 2000.

KP98

Y. Kesten and A. Pnueli.
Modularization and abstraction: The keys to formal verification.
In L. Brim, J. Gruska, and J. Zlatuska, editors, The 23rd International Symposium on Mathematical Foundations of Computer Science, volume 1450 of Lect. Notes in Comp. Sci., pages 54-71. Springer-Verlag, 1998.

KP00a

Y. Kesten and A. Pnueli.
Control and data abstractions: The cornerstones of practical formal verification.
Software Tools for Technology Transfer, 2(1):328-342, 2000.

KP00b

Y. Kesten and A. Pnueli.
Verification by finitary abstraction.
Information and Computation, a special issue on Compositionality, 163:203-243, 2000.

KPR98

Y. Kesten, A. Pnueli, and L. Raviv.
Algorithmic verification of linear temporal logic specifications.
In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proc. 25th Int. Colloq. Aut. Lang. Prog., volume 1443 of Lect. Notes in Comp. Sci., pages 1-16. Springer-Verlag, 1998.

KPRS01

Y. Kesten, A. Pnueli, L. Raviv, and E. Shahar.
Ltl model checking with strong fairness.
Formal Methods in System Design, 2001.
Submitted.

KPSY99

Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine.
Decidable intergation graphs.
Information and Computation, 150(2):209-243, 1999.

KPV00

O. Kupferman, N. Piterman, and M.Y. Vardi.
Fair equivalence relations.
In S. Kapoor and S. Prasad, editors, FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lect. Notes in Comp. Sci., pages 151-163. Springer-Verlag, 2000.

KPV01a

Y. Kesten, A. Pnueli, and M. Vardi.
Verification by augmented abstraction: The automata theoretic view.
J. Comp. Systems Sci., 2001.
To Appear.

KPV01b

O. Kupferman, N. Piterman, and M. Vardi.
Extended temporal logic revisited.
In Proceedings Conference on Concurrency Theory, August 2001.
To appear.

Lam79

L. Lamport.
How to make a multiprocessor computer that correctly executes multiprocess programs.
IEEE Transactions on Computers, C-82(9):690-691, 1979.

LPZ85

O. Lichtenstein, A. Pnueli, and L. Zuck.
The glory of the past.
In Proc. Conf. Logics of Programs, volume 193 of Lect. Notes in Comp. Sci., pages 196-218. Springer-Verlag, 1985.

LW00

E.S. Lander and A.R. Weinberg.
Genomics: journey to the center of biology.
Science, 287:1777-1782, 2000.

McM93

K.L McMillan.
Symbolic Model Checking.
Kluwer Academic Publishers, Boston, 1993.

Mor98

P.A. Morel.
Mathematical modeling of immunological reactions.
Front Biosci, 3:338-347, 1998.

MP95

Z. Manna and A. Pnueli.
Temporal Verification of Reactive Systems: Safety.
Springer-Verlag, New York, 1995.

MPS95

O. Maler, A. Pnueli, and J. Sifakis.
On the synthesis of discrete controllers for timed systems.
In E.W. Mayr and C. Puech, editors, Proceedings of STACS'95, volume 900 of Lect. Notes in Comp. Sci., pages 229-242. Springer-Verlag, 1995.

OSRSC99

S. Owre, N. Shankar, J.M. Rushby, and D.W.J. Stringer-Calvert.
PVS System Guide.
Menlo Park, CA, September 1999.

Pit00

N. Piterman.
Extending temporal logic with $\omega$-automata.
Master's thesis, Weizmann Institute of Science, Israel, 2000.
Available in http://www.wisdom.weizmann.ac.il/home/nirp/public_html/publications/msc_th esis.ps.

PRSS99

A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel.
Deciding equality formulas by small-domains instantiations.
In N. Halbwachs and D. Peled, editors, Proc. 11^st Intl. Conference on Computer Aided Verification (CAV'99), volume 1633 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 455-469, 1999.

PRZ01

A. Pnueli, S. Ruah, and L. Zuck.
Automatic deductive verification with invisible invariants.
In Proc. 7^th Intl. Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), volume 2031, pages 82-97, 2001.

PS96

A. Pnueli and E. Shahar.
A platform for combining deductive with algorithmic verification.
In R. Alur and T. Henzinger, editors, Proc. 8^th Intl. Conference on Computer Aided Verification (CAV'96), volume 1102 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 184-195, 1996.

PS00

A. Pnueli and E. Shahar.
Liveness and acceleration in parameterized verification.
In A. Emerson and P. S. Sistla, editors, Proc. 12^nd Intl. Conference on Computer Aided Verification (CAV'00), volume 1855 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 328-343, 2000.

PSS98a

A. Pnueli, M. Siegel, and O. Shtrichman.
The code validation tool (CVT)- automatic verification of a compilation process.
Software Tools for Technology Transfer, 2(2):192-201, 1998.

PSS98b

A. Pnueli, M. Siegel, and O. Shtrichman.
Translation validation for synchronous languages.
In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proc. 25th Int. Colloq. Aut. Lang. Prog., volume 1443 of Lect. Notes in Comp. Sci., pages 235-246. Springer-Verlag, 1998.

PSS00

A. Pnueli, M. Siegel, and O. Shtrichman.
Translation validation: From SIGNAL to C.
In E.-R. Olderog and B. Steffen, editors, Correct System Design, volume 1710 of LNCS State-of-the-Art Survey, pages 231-255. Springer-Verlag, 2000.

PV94

A. Puri and P. Varaiya.
Decidability of hybrid systems with rectangular differential equations.
In D. L. Dill, editor, Proc. 6th Conference on Computer Aided Verification, volume 818 of Lect. Notes in Comp. Sci., pages 95-104. Springer-Verlag, 1994.

PZP00

A. Pnueli, L. Zuck, and P. Pandya.
Translation validation of optimizing compilers by computational induction.
Technical report, Weizmann Institute of Science, 2000.

RA81

G. Ricart and A.K. Agrawala.
An optimal algorithm for mutual exclusion in computer networks.
Comm. ACM, 24(1):9-17, 1981.
Corr. ibid. 1981, p.581.

RP99

S. Ruah and A. Pnueli.
Streamlining deductive verification of hardware designs.
Technical report, Weizmann Institute, 1999.

RS01

Y. Rodeh and O. Shtrichman.
Finite instantiations in equivalence logic with uninterpreted functions.
In Proc. 13^rd Intl. Conference on Computer Aided Verification (CAV'01), Lect. Notes in Comp. Sci., Springer-Verlag, 2001.
To appear.

RSP01

Y. Rodeh, O. Shtrichman, and A. Pnueli.
Dynamic range allocation.
Technical report, Dept. of Applied Mathematics, Weizmann Institute of Science, 2001.

Sha96

E. Shahar.
The TLV system and its applications.
Master's thesis, Weizmann Institute, 1996.

She59

J.C. Shepherdson.
The reduction of two-way automata to one-way automata.
IBM J. Research, 3:198-200, 1959.

Sht00

O. Shtrichman.
Tuning SAT checkers for bounded model-checking.
In A. Emerson and P. S. Sistla, editors, Proc. 12^nd Intl. Conference on Computer Aided Verification (CAV'00), volume 1855 of Lect. Notes in Comp. Sci., Springer-Verlag, pages 480-494, 2000.

Sht01

O. Shtrichman.
Pruning techniques for the bounded model checking problem.
In Proc. of the Internatinal Conference on Correct Hardware Design and Verification Methods (CHARME01), Edinburgh, 2001. Chapmann & Hall.
(to appear).

SPBA00

E. Sedletsky, A. Pnueli, and M. Ben-Ari.
Formal verification of the ricart-agrawala algorithm.
In S. Kapoor and S. Prasad, editors, FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science, volume 1974 of Lect. Notes in Comp. Sci., pages 325-335. Springer-Verlag, 2000.

Szy88

B. K. Szymanski.
A simple solution to Lamport's concurrent programming problem with linear wait.
In Proc. 1988 International Conference on Supercomputing Systems, pages 621-626, St. Malo, France, 1988.

UML

UML.
Documentation of the unified modeling language (UML).
Available from the Object Management Group (OMG), http://www.omg.org.

VW94

M.Y. Vardi and P. Wolper.
Reasoning about infinite computations.
Inf. and Cont., 115(1):1-37, 1994.

WL89

P. Wolper and V. Lovinfosse.
Verifying properties of large sets of processes with network invariants.
In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, volume 407 of Lect. Notes in Comp. Sci., pages 68-80. Springer-Verlag, 1989.

Yea96

K.C. Yeager.
The Mips r10000 super-scalar microprocessor.
IEEE Micro, April 1996.

ZPL00

L. Zuck, A. Pnueli, and R. Leviathan.
Validations of optimizing compliers.
Technical report, Weizmann Institute of Science, 2000.