Bibliography

1

Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani.
Automatic predicate abstraction of C programs.
In Proceedings of the SIGPLAN '01 Conference on Programming Language Design and Implementation, 2001.

2

Boris Beizer.
Software Testing Techniques.
Electrical/Computer Science and Engineering Series. Van Nostrand Reinhold, 1983.

3

Edoardo Biagioni.
A structured TCP in standard ML.
In SIGCOMM, pages 36-45, 1994.

4

T. Bolognesi and E. Brinksma.
Introduction to the iso specification language lotos.
In Computer Networks and ISDN Systems, pages 14:25-59, 1986.

5

Frederic Boussinot and Robert de Simone.
The esterel language.
Technical report, INRIA Sophia-Antipolis, July 1991.

6

R. Braden.
Requirements for internet hosts - communication layers.
RFC 1122, USC/Information Sciences Institute, October 1989.

7

Lawrence S. Brakmo and Larry L. Peterson.
Experiences with network simulation.
In Measurement and Modeling of Computer Systems, pages 80-90, 1996.

8

G. Brat, K. Havelund, S. Park, and W. Visser.
Model checking programs.
In IEEE International Conference on Automated Software Engineering (ASE), 2000.

9

W.R. Bush, J.D. Pincus, and D.J. Sielaff.
A static analyzer for finding dynamic programming errors.
Software: Practice and Experience, 30(7):775-802, 2000.

10

C.N. Ip and D.L. Dill.
Better verification through symmetry.
In D. Agnew, L. Claesen, and R. Camposano, editors, Computer Hardware Description Languages and their Applications, pages 87-100, Ottawa, Canada, 1993. Elsevier Science Publishers B.V., Amsterdam, Netherland.

11

Douglas Comer and John C. Lin.
Probing TCP implementations.
In USENIX Summer, pages 245-255, 1994.

12

C.Perkins, E. Royer, and S. Das.
Ad Hoc On Demand Distance Vector (AODV) Routing.
IETF Draft, https://www.ietf.org/internet-drafts/draft-ietf-manet-aodv-10.txt, January 2002.

13

Manuvir Das, Sorin Lerner, and Mark Seigle.
Esp: Path-sensitive program verification in polynomial time.
In Conference on Programming Language Design and Implementation, 2002.

14

Scott Dawson, Farnam Jahanian, and Todd Mitton.
Experiments on six commercial TCP implementations using a software fault injection tool.
Software Practice and Experience, 27(12):1385-1410, 1997.

15

R. DeLine and M. Fähndrich.
Enforcing high-level protocols in low-level software.
In Proceedings of the ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation, June 2001.

16

C. Flanagan, K.R.M. Leino, M. Lillibridge, G. Nelson, J.B. Saxe, and R. Stata.
Extended static checking for Java.
In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, pages 234-245. ACM Press, 2002.

17

Cormac Flanagan and Stephen N. Freund.
Type-based race detection for Java.
In SIGPLAN Conference on Programming Language Design and Implementation, pages 219-232, 2000.

18

J.S. Foster, T. Terauchi, and Alex Aiken.
Flow-sensitive type qualifiers.
In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, June 2002.

19

D. Frigioni, A. Marchetti-Spaccamela, and U. Nanni.
Incremental algorithms for single-source shortest path trees.
In Proceedings of Foundations of Software Technology and Theoretical Computer Science, pages 112-224, 1994.

20

P. Godefroid.
Model Checking for Programming Languages using VeriSoft.
In Proceedings of the 24th ACM Symposium on Principles of Programming Languages, 1997.

21

N.C. Hutchinson and L.L. Peterson.
The x-kernel: an architecture for implementing network protocols.
IEEE Trans. on Soft. Eng., 17(1), January 1991.

22

Radu Iosif.
Exploiting Heap Symmetries in Explicit-State Model Checking of Software.
In Proceedings of 16th IEEE Conference on Automated Software Engineering, 2001.

23

P. Keleher, S. Dwarkadas, A. L. Cox, and W. Zwaenepoel.
Treadmarks: Distributed shared memory on standard workstations and operating systems.
In Proc. of the Winter 1994 USENIX Conference, pages 115-131, 1994.

24

Eddie Kohler, M. Frans Kaashoek, and David R. Montgomery.
A readable TCP in the prolac protocol language.
In SIGCOMM, pages 3-13, 1999.

25

S. McCanne and S. Floyd.
UCB/LBNL/VINT network simulator - ns (version 2), April 1999.
https://www.isi.edu/nsnam/ns/.

26

K.L. McMillan and J. Schwalbe.
Formal verification of the gigamax cache consistency protocol.
In Proceedings of the International Symposium on Shared Memory Multiprocessing, pages 242-51. Tokyo, Japan Inf. Process. Soc., 1991.

27

Allen Brady Montz, David Mosberger, Sean W. O'Malley, Larry L. Peterson, Todd A. Proebsting, and John H. Hartman.
Scout: A communications-oriented operating system (abstract).
In Operating Systems Design and Implementation, page 200, 1994.

28

Madanlal Musuvathi.
CMC: A model checker for network protocol implementations.
Technical Report PhD Thesis, Stanford University, January 2004.
https://verify.stanford.edu/madan/thesis/main.pdf.

29

Madanlal Musuvathi and Dawson R. Engler.
Checking system rules using system-specific, programmer-written compiler extensions.
In Proceedings of Operating Systems Design and Implementation (OSDI), September 2000.

30

Madanlal Musuvathi, David Park, Andy Chou, Dawson R. Engler, and David L. Dill.
CMC: A Pragmatic Approach to Model Checking Real Code.
In Proceedings of the Fifth Symposium on Operating Systems Design and Implementation, December 2002.

31

Paolo Narvaez, Kai-Yeung Siu, and Hong-Yi Tzeng.
New dynamic SPT algorithm based on a ball-and-string model.
In INFOCOM (2), pages 973-981, 1999.

32

G. Nelson.
Techniques for program verification.
Available as Xerox PARC Research Report CSL-81-10, June, 1981, Stanford University, 1981.

33

Vern Paxson.
Automated packet trace analysis of TCP implementations.
In SIGCOMM, pages 167-179, 1997.

34

Vern Paxson and et.al.
Known TCP Implementation Problems.
RFC 2525, March 1999.

35

J. Postel.
Transmission control protocol.
RFC 793, USC/Information Sciences Institute, September 1981.

36

U. Stern and D. L. Dill.
A New Scheme for Memory-Efficient Probabilistic Verification.
In IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, 1996.

37

U. Stern and D.L. Dill.
Automatic verification of the SCI cache coherence protocol.
In Correct Hardware Design and Verification Methods: IFIP WG10.5 Advanced Research Working Conference Proceedings, 1995.

38

The User-mode Linux Kernel.
https://user-mode-linux.sourceforge.net/.