S. Park. "Computer Assisted Analysis of Multiprocessor Memory Systems."
Ph.D. Dissertation. Stanford University, June 1996. [Abstract]
A Book Chapter
Co-authored with SPARC Committee. "Chapter: Formal Specification of the Memory Models." In
Architecture Manual Version 9, (ISBN 0-13-099227-5), Edited by D. Weaver and T. Germond, pages 255-266. Prentice Hall, 1994.
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,
"Verifying time partitioning in the DEOS scheduling kernel."
Formal Methods in System Design,
volume 26(2), pages 103-135, March 2005.
W. Visser, K. Havelund, G. Brat, S. Park, F. Lerda.
"Model checking programs."
Automated Software Engineering, volume 10(2), pages 203-232, April 2003.
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.
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]
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]
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.
D. Dai, et al. "FPGA-based prototyping of a 2D Mesh/Torus on-chip interconnect." In Proceedings of the 18th Annual ACM/SIGDA International Symposium on Field Programmable Gate Arrays, February 2010.
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),
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,
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
RMO (Relaxed Memory Order)." In Proceedings of 7th ACM Symposium
on Parallel Algorithms and Architectures, pages 34-41, July 1995.
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.