Publications of Henrik Reif Andersen

There is a bibtex file with the references. Papers with key "IT-TR-yyyy-nnn" or "ID-TR:yyyy-nn" are published as Technical Reports available in hardcopy from the Department of Information Technology, Technical University of Denmark (mail to: aaa@it.dtu.dk).

References

IT-TR-1999-024
More info on the DDD Download Page
Jesper Møller, Jakob Lichtenberg, Henrik Reif Andersen, and Henrik Hulgaard. On the Symbolic Verification of Timed Systems, Technical Report IT-TR-1999-024, Department of Information Technology, Technical University of Denmark, February 1999.

IT-TR-1999-023
More info on the DDD Download Page
Jesper Møller, Jakob Lichtenberg, Henrik Reif Andersen, and Henrik Hulgaard. Difference Decision Diagrams, Technical Report IT-TR-1999-023, Department of Information Technology, Technical University of Denmark, February 1999.

CAV99
Abstract, PostScript (gzip'ed)
Jørn Lind-Nielsen, Henrik Reif Andersen. Stepwise CTL Model Checking of State/Event Systems. Accepted for CAV'99.

TCAD99
Henrik Hulgaard, Poul Frederick Williams, Henrik Reif Andersen. Combinational Logic-Level Verification using Boolean Expression Diagrams. Accepted for TCAD.

TACAS99
Gerd Berhmann, Kim G. Larsen, Henrik Reif Andersen, Henrik Hulgaard, Jørn Lind-Nielsen. Verification of Hierarchical State/Event Systems using Reusability and Compositionality. In the Fifth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 1999. To appear.

STTT98
Abstract, Off-prints: mail to hra@it.dtu.dk
Henrik Reif Andersen, Jørn Lind-Nielsen. Partial Model Checking of Modal Equations: A Survey. In Software Tools for Technology Transfer, volume 2 number 3, Springer-Verlag 1999.

TACAS98
Abstract, PostScript, PostScript (gzip'ed)
Jørn Lind-Nielsen, Henrik Reif Andersen, Gerd Behrmann, Henrik Hulgaard, Kåre Kristoffersen, Kim G. Larsen Verification of Large State/Event Systems using Compositionality and Dependency Analysis. Appears in Proceedings of TACAS'98, Bernhard Steffen (ed), LNCS 1384, April 1998. Springer-Verlag. NOTE: The technique described in this paper is being patented by Baan Visualstate (formerly Beologic), which has all commercial rights.

RM97
Abstract, PostScript, PostScript (gzip'ed)
Henrik Hulgaard, Poul Frederick Williams, Henrik Reif Andersen. Combinational Logic-Level Verification using Boolean Expression Diagrams. In 3rd International Workshop on Applications of the Reed-Muller Expansion in Circuit Design, Sept. 1997.

CONCUR97
Abstract, PostScript, PostScript (gzip'ed)
Henrik Reif Andersen, Simon Mørk, Morten Ulrik Sørensen. A Universal Reactive Machine. In Proceedings of CONCUR'97: Concurrency Theory, 8th International Conference, LNCS 1243, July 1997, pp. 89-103. Springer-Verlag.

LICS97
Abstract, PostScript, PostScript (gzip'ed)
Henrik Reif Andersen, Henrik Hulgaard. Boolean Expression Diagrams. In Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29-July 2, 1997, pp. 88-98. IEEE Computer Society.

TACAS97
Abstract, PostScript, PostScript (gzip'ed)
Henrik Reif Andersen, Jørgen Staunstrup, and Niels Maretti. Partial Model Checking with ROBDDs. In Proceedings of TACAS'97, LNCS 1217, 1997, pp. 35-49. Springer-Verlag.

FASE97
Abstract, PostScript, PostScript (gzip'ed)
Henrik Reif Andersen, Jørgen Staunstrup, and Niels Maretti. A Comparison of Modular Verification Techniques. In Proceedings of TAPSOFT'97, LNCS 1214, 1997, pp. 550-564. Springer-Verlag.

CONCUR96
Abstract
Henrik Reif Andersen and Jørn Lind-Nielsen. MuDiv: A Tool for Partial Model Checking. Demonstration at CONCUR'96, Pisa, 26-29 August, 1996.

HYBRID95
Abstract
Jakob Lyng Petersen and Henrik Reif Andersen. Specification of a Real-Time Pulse Detector. 1995. Presented at the Second European Workshop on Hybrid Systems, May 31-June 2, 1995, Grenoble, France.

CAV95
Abstract, PostScript, PostScript (gzip'ed), DVI, DVI (gzip'ed)
Henrik Reif Andersen and Bart Vergauwen. Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion. January 1995. 13 pp. Appears in Proceedings of CAV'95, Liege, Belgium, July 3-5, 1995. LNCS 939, Springer-Verlag, pp. 142-154.

LICS95
Abstract, PostScript, PostScript (gzip'ed)
Henrik Reif Andersen. Partial Model Checking (Extended Abstract). June 1995. 10 pp. Appears in Proceedings of LICS'95. La Jolla, San Diego, June 26-29, 1995, IEEE Computer Society Press, pp. 398-407.

TAPSOFT95
Abstract, PostScript, PostScript (gzip'ed)
Henrik Reif Andersen and Michael Mendler. Describing a Signal Analyzer in the Process Algebra PMC - A Case Study. 16 pp. Appears in Proceedings of TAPSOFT'95, pp. 620-635, Aarhus, Denmark, May 1995, Springer-Verlag, LNCS 915.

ID-TR:1994-145
Abstract, PostScript, PostScript (gzip'ed), DVI, DVI (gzip'ed)
Henrik Reif Andersen. A Polyadic Modal mu-Calculus. August 1994. 16 pp.

LFCS94
Abstract, PostScript, PostScript (gzip'ed), DVI, DVI (gzip'ed)
Henrik Reif Andersen. On Model Checking Infinite-State Systems. July 1994. 13 pp. Appears in: Proceedings of LFCS'94. Pages 8-17. LNCS 813. Springer-Verlag.

LICS94
Abstract, PostScript, PostScript (gzip'ed)
Henrik Reif Andersen, Colin Stirling, and Glynn Winskel. A Compositional Proof System for the Modal mu-Calculus. July 1994. 18 pp. Also as BRICS Report RS-94-34. Appears in: Proceedings of LICS'94. IEEE Computer Society Press.

ESOP94
Abstract, PostScript, PostScript (gzip'ed), DVI, DVI (gzip'ed)
Henrik Reif Andersen and Michael V. Mendler. An Asynchronous Process Algebra with Multiple Clocks. April 1994. 16 pp. Appears in: Proceedings of ESOP'94. LNCS 788. Springer-Verlag.

TCS94
Abstract, Off-prints: mail to hra@it.dtu.dk
Henrik Reif Andersen. Model Checking and Boolean Graphs. April 1994. 28 pp. Appears in: Theoretical Computer Science, 126:1, pages 3-30, April 1994. Elsevier.

ID-TR:1993-126
Abstract, PostScript, PostScript (gzip'ed)
Henrik Reif Andersen and Michael V. Mendler. Complete Axiomatization of Observation Congruence for PMC. December 1993.

ID-TR:1993-122
Abstract, PostScript, PostScript (gzip'ed)
Henrik Reif Andersen and Michael V. Mendler. A Process Algebra with Multiple Clocks. August 1993.

THESIS
Abstract, PostScript, pdf, Hardcopy: mail to kkmoller@daimi.aau.dk
Henrik Reif Andersen. Verification of Temporal Properties of Concurrent Systems, viii+203 pages. Department of Computer Science, Aarhus University, Denmark. Report PB-445, June 1993.

DAIMI-PB-446
Abstract, Hardcopy: mail to kkmoller@daimi.aau.dk
Henrik Reif Andersen. On Reasoning about Infinite State Systems in the Modal mu-calculus. Computer Science Department, Aarhus University, Denmark. Report PB-446, June 1993. Revised version: See LFCS94 above.

DAIMI-PB-420
Abstract, Hardcopy: mail to kkmoller@daimi.aau.dk
Henrik Reif Andersen. Local Computation of Simultaneous Fixed-Points Computer Science Department, Aarhus University, Denmark. Report PB-420, October 1992.

CLCAM-260
Abstract
Henrik Reif Andersen. Local Computation of Alternating Fixed-Points. Technical Report No. 260, Computer Laboratory, University of Cambridge. June 1992.

FMSD92
Abstract, Off-prints: mail to hra@it.dtu.dk
Henrik Reif Andersen and Glynn Winskel. Compositional Checking of Satisfaction. In Formal Methods in System Design, 1(4), December 1992.

ESOP92
Abstract
Henrik Reif Andersen. Model Checking and Boolean Graphs (Extended Abstract) In Proceedings of ESOP'92. Journal version as TCS94 above.

CAV91
Abstract
Henrik Reif Andersen and Glynn Winskel. Compositional Checking of Satisfaction (Extended Abstract) In Proceedings of CAV'91. Journal version as FMSD92 above.


Comments to: hra@itu.dk (Henrik Reif Andersen)