|
Jens Ulrik Skakkebækjus@cs.stanford.edu
|
Please Note
I have left Stanford to join a start-up: BV2000, Inc. To contact me, send an email to: jskakkebaek@bv2000.com.
Selected Publications
The papers are in compressed PostScript format.Software
- Applying Model Checking in JAVA Verification by Klaus Havelund and Jens U. Skakkebæk. Accepted to 6th SPIN Workshop '99 (held in connection with FM'99, September, Toulouse, France).
- Reducing Manual Abstraction in Formal Verification of Out-of-Order Execution by Robert B. Jones, Jens U. Skakkebæk, and David L. Dill. In Formal Methods in Computer Aided Design (FMCAD), volume 1522 of Lecture Notes in Computer Science, pages 2--17, Springer-Verlag, November 1998.
- Formally Verifying Data and Control with Weak Reachability Invariants by Jeffrey Su, David L. Dill, and Jens U. Skakkebæk. Formal Methods in Computer Aided Design (FMCAD), volume 1522 of Lecture Notes in Computer Science, Springer-Verlag, November 1998.
- Formal Verification of Out-of-Order Execution Using Incremental Flushing by Jens U. Skakkebæk, Robert B. Jones, and David L. Dill. In Computer Aided Verification (CAV) '98, volume 1427 of Lecture Notes in Computer Science, pages 98--109. Springer-Verlag, June 1998.
- Static Analysis to Identify Invariants in RSML Specifications by David Y.W. Park, Jens U. Skakkebæk, and David L. Dill. To appear in Formal Techniques in Real-Time and Fault Tolerant Systems, Lyngby, Denmark, September 1998.
- Checking Properties of Safety Critical Specifications Using Efficient Decision Procedures by David Y.W. Park, Jens U. Skakkebæk, Mats P.E. Heimdahl, Barbara J. Czerny, and David L. Dill. In proceedings of FMSP'98: Second Workshop on Formal Methods in Software Practice, March 1998, pages 34--43, ACM press.
- Refining System Requirements to Program Specification by E.-R. Olderog, A.P. Ravn, and Jens Ulrik Skakkebæk, in Formal Methods for Real-Time Computing, eds. C. Heitmeyer and D. Mandrioli, Trends in Software, Vol. 5, pp. 107-134, Wiley, 1996.
- A Verification Assistant for a Real-Time Logic by Jens Ulrik Skakkebæk, Ph.D. Thesis, Department of Computer Science, Technical University of Denmark, Lyngby, Denmark, 1994. Also available as Technical Report ID-TR: 1994-150.
- Towards a Duration Calculus Proof Assistant in PVS by J.U. Skakkebæk and N. Shankar, Formal Techniques in Real-Time and Fault Tolerant Systems, eds. G. Goos, J. Hartmanis, and J. van Leeuwen, Lecture Notes in Computer Science, Vol. 863, pp. 660-679,Springer-Verlag, 1994.
- Liveness and Fairness in Duration Calculus by J.U. Skakkebæk, in CONCUR '94: Concurrency Theory , eds. B. Jonsson and J. Parrow, Lecture Notes in Computer Science, Vol. 836, pp. 283-298,Springer-Verlag, 1994.
- Specification of Embedded Real-Time Systems by J.U. Skakkebæk, A.P. Ravn, H. Rischel and Zhou Chaochen, IEEE Workshop on Real-Time Systems, pp. 116-121, June, 1992.
Background
From June 1st, 1996, to September 15, 1999, I worked as a research associate at the Computer
Science Department at Stanford University,
where I work in Prof. David Dill's
research group in the area of
formal verification. From March 1995 to May 1996 I worked as a Software
Engineer in the On-Board Software
Department, Space Division,
Computer Resources International. From
September 1991 to August 1994 I did my Ph.D. at Department of Computer
Science (now Department of Information
Technology) at the Technical University
of Denmark. Supervisors were Anders
Ravn and Hans Rischel.
During my Ph.D. I worked for 10 months in 1993 as a Research Associate
in the Formal Methods
Group headed by John
Rushby of the Computer Science Laboratory,
SRI International. In particular, I worked
with N. Shankar
and Sam Owre to use PVS
as a basis to build a proof assistant for Duration Calculus.
Research Interests
Formal verification: theorem proving, model checking, other finite state
methods; embedded, real-time systems; real-time and modal logics; fault
tolerance, safety critical systems.
Software
The original Duration Calculus extension to PVS version 1, called PC/DC, comes with a README file and an announcement.
PC/DC has been updated to PVS 2.2 by Soeren Heilmann and can be found
here.
Links
The Hardware Verification Group
Teaching
In Fall '98 I co-taught CS444: Software Development of Safety-Critical Applications.
Other
I was on the program committee of Formal Methods in Computer Aided Design (FMCAD '98).
Maps
Stanford Campus Map zoomed in on the Gates Building
Contact Address
-
Send an email to: jskakkebaek@bv2000.com