cs0608035/main.bbl
1: \begin{thebibliography}{10}
2: 
3: \bibitem{SLAM}
4: T.~Ball, B.~Cook, V.~Levin, and S.~K. Rajamani.
5: \newblock Slam and static driver verifier: Technology transfer of formal
6:   methods inside microsoft.
7: \newblock In {\em Integrated Formal Methods 2004}, volume 2999 of {\em
8:   Springer-Verlag}, pages 1--20, 2004.
9: 
10: \bibitem{Ball02POPL}
11: T.~Ball and S.~K. Rajamani.
12: \newblock The {SLAM} project: Debugging system software via static analysis.
13: \newblock In {\em {Proceedings of {ACM} SIGPLAN/SIGACT Symposium on Principles
14:   of Programming Languages}}, pages 1--3, 2002.
15: 
16: \bibitem{Rehof02POPL}
17: S.~Chaki, S.~Rajamani, and J.~Rehof.
18: \newblock Types as models: Model checking message-passing programs.
19: \newblock In {\em {Proceedings of {ACM} SIGPLAN/SIGACT Symposium on Principles
20:   of Programming Languages}}, pages 45--57, 2002.
21: 
22: \bibitem{Flanagan03PLDI}
23: S.~Q. Cormac~Flanagan.
24: \newblock A type and effect system for atomicity.
25: \newblock In {\em Proceedings of {{ACM} SIGPLAN Conference on Programming
26:   Language Design and Implementation}}, pages 338--349, 2003.
27: 
28: \bibitem{DeLine01PLDI}
29: R.~DeLine and M.~F{\"{a}}hndrich.
30: \newblock Enforcing high-level protocols in low-level software.
31: \newblock In {\em Proceedings of {{ACM} SIGPLAN Conference on Programming
32:   Language Design and Implementation}}, pages 59--69, 2001.
33: 
34: \bibitem{DeLine02PLDI}
35: R.~DeLine and M.~F{\"{a}}hndrich.
36: \newblock Adoption and focus: Practical linear types for imperative
37:   programming.
38: \newblock In {\em Proceedings of {{ACM} SIGPLAN Conference on Programming
39:   Language Design and Implementation}}, 2002.
40: 
41: \bibitem{Aiken02PLDI}
42: J.~S. Foster, T.~Terauchi, and A.~Aiken.
43: \newblock Flow-sensitive type qualifiers.
44: \newblock In {\em Proceedings of {{ACM} SIGPLAN Conference on Programming
45:   Language Design and Implementation}}, pages 1--12, 2002.
46: 
47: \bibitem{Rehof04CAV}
48: C.~Fournet, T.~Hoare, S.~K. Rajamani, and J.~Rehof.
49: \newblock Stuck-free conformance.
50: \newblock In {\em CAV'04}, volume 3114 of {\em {Lecture Notes in Computer
51:   Science}}, pages 242--254. Springer-Verlag, 2004.
52: 
53: \bibitem{Honda02POPL}
54: K.~Honda and N.~Yoshida.
55: \newblock A uniform type structure for secure information flow.
56: \newblock In {\em {Proceedings of {ACM} SIGPLAN/SIGACT Symposium on Principles
57:   of Programming Languages}}, pages 81--92, 2002.
58: 
59: \bibitem{Kobayashi03TCS}
60: A.~Igarashi and N.~Kobayashi.
61: \newblock A generic type system for the pi-calculus.
62: \newblock {\em {Theoretical Computer Science}}, 311(1-3):121--163, 2004.
63: 
64: \bibitem{IK05TOPLAS}
65: A.~Igarashi and N.~Kobayashi.
66: \newblock Resource usage analysis.
67: \newblock {\em {ACM Transactions on Programming Languages and Systems}},
68:   27(2):264--313, 2005.
69: \newblock Preliminary summary appeared in Proceedings of POPL 2002.
70: 
71: \bibitem{TyPiCal}
72: N.~Kobayashi.
73: \newblock Typical: A type-based static analyzer for the pi-calculus.
74: \newblock Tool available at
75:   \url{http://www.kb.ecei.tohoku.ac.jp/~koba/typical/}.
76: 
77: \bibitem{Kobayashi98TOPLAS}
78: N.~Kobayashi.
79: \newblock A partially deadlock-free typed process calculus.
80: \newblock {\em {ACM Transactions on Programming Languages and Systems}},
81:   20(2):436--482, 1998.
82: 
83: \bibitem{Kobayashi02IC}
84: N.~Kobayashi.
85: \newblock A type system for lock-free processes.
86: \newblock {\em {Information and Computation}}, 177:122--159, 2002.
87: 
88: \bibitem{Kobayashi05ActInf}
89: N.~Kobayashi.
90: \newblock Type-based information flow analysis for the pi-calculus.
91: \newblock {\em Acta Informatica}, 42(4-5):291--347, 2005.
92: 
93: \bibitem{Kobayashi00CONCUR}
94: N.~Kobayashi, S.~Saito, and E.~Sumii.
95: \newblock An implicitly-typed deadlock-free process calculus.
96: \newblock In {\em Proceedings of CONCUR2000}, volume 1877 of {\em {Lecture
97:   Notes in Computer Science}}, pages 489--503. Springer-Verlag, August 2000.
98: 
99: \bibitem{Marriott03}
100: K.~Marriott, P.~J. Stuckey, and M.~Sulzmann.
101: \newblock Resource usage verification.
102: \newblock In {\em Proceedings of the First Asian Symposium on Programming
103:   Languages and Systems (APLAS 2003)}, volume 2895 of {\em {Lecture Notes in
104:   Computer Science}}, pages 212--229, 2003.
105: 
106: \bibitem{MayrPetriNet}
107: E.~W. Mayr.
108: \newblock An algorithm for the general petri net reachability problem.
109: \newblock {\em SIAM Journal on Computing}, 13(3):441--461, 1984.
110: 
111: \bibitem{Milner89CCS}
112: R.~Milner.
113: \newblock {\em Communication and Concurrency}.
114: \newblock Prentice Hall, 1989.
115: 
116: \bibitem{Rathke2005}
117: N.~Nguyen and J.~Rathke.
118: \newblock Typed static analysis for concurrent, policy-based, resource access
119:   control.
120: \newblock draft.
121: 
122: \bibitem{Pelz87}
123: E.~Pelz.
124: \newblock Closure properties of deterministic petri nets.
125: \newblock In {\em STACS 87: 4th Annual Symposium on Theoretical Aspects of
126:   Computer Science}, volume 247 of {\em {Lecture Notes in Computer Science}},
127:   pages 371--382. Springer-Verlag, 1987.
128: 
129: \bibitem{PetriBook}
130: J.~L. Peterson.
131: \newblock {\em Petri Net Theory and the Modeling of Systems}.
132: \newblock Prentice-Hall, 1981.
133: 
134: \bibitem{Rehof04ISOLA}
135: S.~K. Rajamani and J.~Rehof.
136: \newblock Models for contract conformance.
137: \newblock In {\em ISOLA2004, First International Symposium on Leveraging
138:   Applications of Formal Methods}, 2004.
139: 
140: \bibitem{Skalka04}
141: C.~Skalka and S.~Smith.
142: \newblock History effects and verification.
143: \newblock In {\em Proceedings of the First Asian Symposium on Programming
144:   Languages and Systems (APLAS 2004)}, volume 3302 of {\em {Lecture Notes in
145:   Computer Science}}, pages 107--128, 2004.
146: 
147: \bibitem{Yoshida96FST}
148: N.~Yoshida.
149: \newblock Graph types for monadic mobile processes.
150: \newblock In {\em FST/TCS'16}, volume 1180 of {\em {Lecture Notes in Computer
151:   Science}}, pages 371--387. Springer-Verlag, 1996.
152: 
153: \bibitem{Yoshida02liveness}
154: N.~Yoshida.
155: \newblock Type-based liveness guarantee in the presence of nontermination and
156:   nondeterminism.
157: \newblock Technical Report 2002-20, MSC Technical Report, University of
158:   Leicester, April 2002.
159: 
160: \end{thebibliography}
161: