Program Analysis Interest Group
   

Books

  • Logic in Computer Science: modelling and reasoning about systems. Michael Huth and Mark Ryan. Cambridge University Press, Second Edition. July 2004. ( book )
  • An abstraction framework for mixed non-deterministic and probabilistic systems. Michael Huth. Book chapter in C. Baier et al. (Eds.): Validation of Stochastic Systems, LNCS 2925, pp. 419--444, Springer Verlag Berlin Heidelberg, July 2004.
  • Secure communicating systems: design, analysis, and implementation. Michael Huth. Cambridge University Press. August 2001. ( book )
  • Principles of Program Analysis. Flemming Nielson, Hanne Riis Nielson and Chris Hankin. Springer Verlag, 1999.

Journals

  • Assigning Types to Processes (full version). Nobuko Yoshida and Matthew Hennessy. Journal of Information and Computation, 2004. ( .ps.gz )
  • Noninterference through Flow Analysis. Kohei Honda and Nobuko Yoshida, Revised in June 2004. To appear in Journal of Functional Programming, 2004. ( .ps )
  • A domain equation for partial systems. Michael Huth, Radha Jagedeesan, and David Schmidt. 38pp., Mathematical Structures in Computer Science, vol. 14, issue 4, pp. 469--505, August 2004, Cambridge University Press.
  • Mathematics for the exploration of requirements. Michael Huth. ACM SIGCSE Bulletin Inroads, vol. 35, no. 2, pp. 34--39, June 2004.
  • Approximate Non-Interference. Alessandra Di Pierro, C. Hankin, and H. Wiklicky. Journal of Computer Security, 12(1):37-81, 2004. (ps)
  • Strong Normalisation in the Pi-Calculus (full version). Nobuko Yoshida, Martin Berger and Kohei Honda, Revised August 2003. Journal of Information and Computation. ( .ps )
  • Information Flow for ALGOL-like Languages. D. Clark, C. Hankin and S. Hunt. Computer Languages (Special Issue: Computer Languages and Security) , volume 28 (1), pages 3 -- 28, April 2002. Ed. A. Cortesi and R. Focardi. Elsevier. (ps)

Conferences

  • A Distributed Abstract Machine for Boxed Ambient Calculi. A. Phillips, N. Yoshida and S. Eisenbach. Proceedings of the European Symposium on Programming, (ETAPS'04), LNCS, April 2004 (Barcelona, Spain). ©Springer. ( .ps )
  • SafeDpi: A Language for Controlling Mobile Code. (Extended abstract) Matthew Hennessy, Julian Rathke and Nobuko Yoshida Proc. of 7th International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2004) ( .pdf )
  • A Compositional Program Logic for Polymorphic Higher-Order Functions. Kohei Honda and Nobuko Yoshida, PPDP'2004, 6th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming, ACM Press, 2004. ( .ps )
  • From Process Logic to Program Logic. Kohei Honda. To appear in 9th ACM-SIGPLAN International Conference on Functional Programming (ICFP 04), ACM Press, 2004. ( .ps )
  • Basic Theory of Reduction Congruence for Two Timed Aysnchronous Pi-Calculi (extended abstract) . Martin Berger. Proc. of CONCUR'2004 LNCS, Springer-Verlag, 2004. ( .ps )
  • Channel Dependent Types for Higher-Order Mobile Processes (Part I). Nobuko Yoshida. Extended Abstract appears in Proc. of POPL'2004, Proc. of 31th ACM Symposium on Principles of Programming Languages, ACM Press, 2004. ( .ps )
  • Control in the Pi-Calculus (extended abstract). Kohei Honda, Nobuko Yoshida and Martin Berger. Fourth ACM-SIGPLAN Continuation Workshop (CW'04) ACM, January, 2004 ( .ps )
  • Beyond image-finiteness: labelled transition systems as a Stone space. Michael Huth. In: Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science, pp. 222-231, Turku, Finland, 13-17 July, IEEE Computer Society Press 2004.
  • Probabilistic KLAIM. Alessandra Di Pierro, C. Hankin and H. Wiklicky. In Proceedings of COORDINATION 2004, 6th International Conference on Coordination Languages and Models, Pisa, Italy, February 2004, Rocco De Nicola and Greg Meredith (Eds.) Lecture Notes in Computer Science 2949 Springer 2004. (ps)
  • Two Formal Approaches for Approximating Noninterference Properties (With A. Aldini, M. Bravetti, R. Gorrieri, C. Hankin and H. Wiklicky) In Foundations of Security Analysis and Design II -- Tutorial Lectures, Lecture Notes in Computer Science 2946 Springer 2004.
  • Quantitative Relations and Approximate Process Equivalences. Alessandra Di Pierro, C. Hankin and H. Wiklicky. In Proceedings of CONCUR'03, Marseille, France, September 2003. Roberto Amadio, Denis Lugiez (Eds.) Lecture Notes in Computer Science 2761 Springer 2003. (ps)
  • Genericity and the Pi-Calculus (full version). Martin Berger, Kohei Honda and Nobuko Yoshida. Extended abstract appears in Proc. of 6th International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2003). Last update 19 March 2004. ( .ps )
  • Measuring the Confinement of Concurrent Probabilistic Systems. Alessandra Di Pierro, C. Hankin and H. Wiklicky. In Proceedings of WITS'03 -- 2003 IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS Workshop on Issues in the Theory of Security, Warsaw, Poland, April 2003. (ps)
  • A Uniform Type Structure for Secure Information Flow (full version). Kohei Honda and Nobuko Yoshida, Revised June, 2004. Extended Abstract appears in Proc. of POPL'2002, Proc. of 29th ACM Symposium on Principles of Programming Languages, ACM Press, 2002. ( .ps )
  • Probabilistic Abstract Interpretation and Statistical Testing. Alessandra Di Pierro and H. Wiklicky. Short abstract in Proceedings of PAPM-Probmiv'02 -- 2nd Joint International Workshop on Process Algebra and Performance Modelling and Probabilistic Methods in Verification, Copenhagen, Denmark, 2002. H. Hermanns, R. Segala (Eds.) Lecture Notes in Computer Science 2399 Springer 2002. (Full paper: ps)
  • Approximate Confinement under Uniform Attacks. Alessandra Di Pierro, C. Hankin and H. Wiklicky. In Proceedings of SAS'02 -- Static Analysis, 9th International Symposium, Madrid, Spain, September 17-20, 2002. Manuel V. Hermenegildo, German Puebla (Eds.) Lecture Notes in Computer Science 2477 Springer 2002. (ps)
  • Approximate Non-Interference. Alessandra Di Pierro, C. Hankin and H. Wiklicky. In Proceedings of CSFW'02 -- 15th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia, Canada, 2002. (ps)
  • On Approximate Non-Interference. Alessandra Di Pierro, C. Hankin and H. Wiklicky. In Proceedings of WITS'02 -- 2nd ACM SIGPLAN and IFIP WG 1.7 Workshop on Issues in the Theory of Security, Portland, Oregon, USA, January 2002. (ps)
  • Linearity and Bisimulation (extended abstract). Nobuko Yoshida, Kohei Honda and Martin Berger. Proc. of 5th International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2002) ( .ps.gz )
  • Sequentiality and the Pi-Calculus (full version). Martin Berger, Kohei Honda and Nobuko Yoshida. Extended abstract appeared in Proc. TLCA'01. Last modified on August 12, 2001. ( .ps )
  • Measuring the Precision of Abstract Interpretations. Alessandra Di Pierro and H. Wiklicky. Proc. of LOPSTR 2000, Tenth International Workshop on Logic-based Program Synthesis and Transformation, Lecture Notes in Computer Science, Vol. 2042, pages 147-164, 2001. (ps)
  • Abstraction-based Model Checking using Modal Transition Systems. Patrice Godefroid, Michael Huth, and Radha Jagadeesan. In: Proceedings of the International Conference on Theory and Practice of Concurrency, Lecture Notes in Computer Science 2154, Springer Verlag, pp. 426--440, August 2001.
  • Modal transition systems: a foundation for three-valued program analysis.Michael Huth, Radha Jagadeesan, and David Schmidt. In: Proceedings of the European Symposium on Programming, (editor: D., Sands), Lecture Notes in Computer Science 2028, Springer Verlag, pp. 155--169. April 2001.
  • Secure Information Flow as Typed Process Behaviour (extended abstract). Kohei Honda, Vasco Vasconcelos and Nobuko Yoshida. A revised version appeared in Proc. of European Symposium on Programming (ESOP) 2000, LNCS 1782, pp. 180--199, Springer, 2000. ( .ps.gz )
  • Concurrent Constraint Programming: Towards Probabilistic Abstract Interpretation. Alessandra Di Pierro and H. Wiklicky. Proc. of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP'00), 20-23 September, Montreal, Canada, 2000. (ps.)
  • Minimality and Separation Results on Asynchronous Mobile Processes: representability theorem by concurrent combinators (extended abstract) Nobuko Yoshida, Proc. of CONCUR'98, LNCS, Springer-Verlag, Nice, France, 8--11 September, 1998. The first version in October 1997, Revised in March, June 1998. ( .ps.gz )

Reports/Other

  • Program Logic and Program Analysis Kohei Honda, Nobuko Yoshida and Martin Berger, Draft. August 2004. ( .ps )
  • SafeDpi: A Language for Controlling Mobile Code. (full version) Matthew Hennessy, Julian Rathke and Nobuko Yoshida Technical Report 02/2003, University of Sussex, Oct 2003. Extended Abstract will appear in Proc. of 7th International Conference, Foundations of Software Science and Computer Structures (FoSSaCs 2004) ( .ps )