SEUNGJOON'S PUBLICATIONS

Ph.D. Thesis

  • S. Park. "Computer Assisted Analysis of Multiprocessor Memory Systems." Ph.D. Dissertation. Stanford University, June 1996. [Abstract] [PDF] [Postscript]

    A Book Chapter

  • Co-authored with SPARC Committee. "Chapter: Formal Specification of the Memory Models." In The SPARC Architecture Manual Version 9, (ISBN 0-13-099227-5), Edited by D. Weaver and T. Germond, pages 255-266. Prentice Hall, 1994.

    Journal Articles

  • M. Azimi, et al. "Integration challenges and tradeoffs for terascale architecture." Intel Technology Journal, volume 11(3), August 2007.

  • J. Penix, W. Visser, S. Park, C. Pasareanu, E. Engstrom, A. Larson, N. Weininger. "Verifying time partitioning in the DEOS scheduling kernel." Formal Methods in System Design, volume 26(2), pages 103-135, March 2005. [Abstract]

  • W. Visser, K. Havelund, G. Brat, S. Park, F. Lerda. "Model checking programs." Automated Software Engineering, volume 10(2), pages 203-232, April 2003. [Abstract]

  • M. Azimi, C. Chou, A. Kumar, V. Lee, P. Mannava, S. Park. "Experience with applying formal methods to protocol specification and system architecture." Formal Methods in System Design, volume 22(2), pages 109-116, March 2003. [Abstract]

  • S. Park, S. Das, D. Dill. "Automatic checking of aggregation abstractions through state enumeration." IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, volume 19(10), pages 1202-1210, October 2000. [Abstract] [PDF]

  • S. Park, D. Dill. "An executable specification and verifier for Relaxed Memory Order." IEEE Transactions on Computers, volume 48(2), pages 227-235, February 1999. [Abstract] [PDF]

  • S. Park, D. Dill. "Verification of cache coherence protocols by aggregation of distributed transactions." Theory of Computing Systems, volume 31(4), pages 355-376, July 1998. [Abstract] [PDF]

    Conference Papers

  • C. Chou, P. K. Mannava, S. Park, "A Simple Method for Parameterized Verification of Cache Coherence Protocols." In Formal Methods in Computer-Aided Design (FMCAD 2004), November 2004.

  • N. Dershowitz, D.N. Jayasimha, S. Park, "Bounded Fairness." In Proceedings of the International Symposium on Verification - Theory and Practice, pages 317-331, LNCS 2772, Springer-Verlag, June 2003.

  • W. Visser, G. Brat, K. Havelund, S. Park. "Model checking programs." In 15th IEEE International Conference on Automated Software Engineering, September 2000.

  • W. Visser, S. Park, J. Penix. "Using predicate abstraction to reduce object-oriented programs for model checking." In Third Workshop on Formal Methods in Software Practice, August 2000.

  • G. Brat, K. Havelund, S. Park, W. Visser. "Java Path Finder: Second Generation of a Java Model Checker." In Workshop on Advances in Verification (WAVe) 2000, July 2000.

  • K. Havelund, M. Lowry, S. Park, C. Pecheur, J. Penix, W. Visser, J. White. "Formal analysis of the remote agent before and after flight." In Lfm2000: Fifth NASA Langley Formal Methods Conference, June 2000.

  • S. Das, D. Dill, S. Park. "Experience with Predicate Abstraction." In Computer Aided Verification, 11th International Conference, CAV'99, pages 160-171, LNCS 1633, Springer-Verlag, July 1999. [Postscript]

  • S. Park, S. Das, D. Dill. "Automatic Checking of Aggregation Abstractions Through State Enumeration," IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, pages 207-222, November 1997. [Postscript]

  • S. Park. "Practical Verification of Cache Coherence Algorithms With an Automatic Theorem-Prover," 2nd International Workshop on Verification of Infinite State Systems: Infinity, July 1997.

  • S. Park, D. Dill. "Protocol Verification by Aggregation of Distributed Transactions." In Computer Aided Verification, 8th International Conference, CAV'96, pages 300-310, LNCS 1102, Springer-Verlag, July 1996. [Postscript]

  • S. Park, D. Dill. "Verification of FLASH Cache Coherence Protocol by Aggregation of Distributed Transactions." In Proceedings of 8th ACM Symposium on Parallel Algorithms and Architectures, pages 288-296, June 1996. [Postscript]

  • S. Park, D. Dill. "An Executable Specification, Analyzer and Verifier for RMO (Relaxed Memory Order)." In Proceedings of 7th ACM Symposium on Parallel Algorithms and Architectures, pages 34-41, July 1995. [Postscript]

  • D. Dill, S. Park, A. Nowatzyk. "Formal Specification of Abstract Memory Models." In Research on Integrated Systems: Proceedings of the 1993 Symposium, pages 38-52. MIT Press, March 1993. [Postscript]

  • S. Park, et al. "A Simple DCT-Domain LMS Algorithm for Non-Stationary Signals." In International Symposium on Computer Architecture and Digital Signal Processing, pages 385-388, October 1989.

    Home