@Article{Amt+Ban:TOPLAS-2020,
  author = 	 {Torben Amtoft and Anindya Banerjee},
  title = 	 {A Theory of Slicing for Imperative Probabilistic Programs},
  year = {2020}, 
  issue_date = {April 2020}, 
  publisher = {Association for Computing Machinery}, 
  address = {New York, NY, USA}, 
  volume = {42}, 
  number = {2}, 
  issn = {0164-0925}, 
  url = {https://doi.org/10.1145/3372895}, 
  doi = {10.1145/3372895}, 
  journal = {ACM Trans. Program. Lang. Syst.}, 
  month = apr, 
  articleno = {Article 6}, 
  numpages = {71}, 
  keywords = {probabilistic control-flow graphs, program slicing, Probabilistic programming} }
 


Back to Main page


























                
@InCollection{,
  author = 	 {Torben Amtoft and Kelly Androutsopoulos and David Clark},
  title = 	 {Correctly Slicing Extended Finite State Machines},
  booktitle = 	 {From Lambda Calculus to Cybersecurity Through Program Analysis: Essays Dedicated to Chris Hankin on the Occasion of His Retirement}
  editor = 	 {Alessandra Di Pierro and Pasquale Malacaria and Rajagopal Nagarajan},
  year = 	 {2020},
  publisher = {Springer Verlag},
  series = 	 {LNCS},
  volume = 	 {12065},
  pages = 	 {149--197},
  url       = {https://doi.org/10.1007/978-3-030-41103-9_6},
  doi       = {10.1007/978-3-030-41103-9_6},
  note = 	 {A much preliminary version appears as Research Note RN/13/22 from University College London, Department of Computer Science, December 2013},
}
 


Back to Main page



























@InProceedings{,
  author = 	 {Torben Amtoft and Anindya Banerjee},
  title = 	 {A Theory of Slicing for Probabilistic Control Flow Graphs},
  booktitle = {FoSSaCS'16},
  year = 	 {2016},
  editor = 	 {Bart Jacobs and Christof L{\"{o}}ding},
  volume = 	 {9634},
  series = 	 {LNCS},
  pages = 	 {180--196}
  publisher =    {Springer-Verlag},
  note = 	 {A previous version (with full proofs) appears as Technical report 2015-1, Department of Computing and Information Sciences, Kansas State University, July 2015.}
}
 


Back to Main page


























                       
@InProceedings{ Amt+etal:POST-2012,
  author = 	 {Torben Amtoft and Josiah Dodds and Zhi Zhang and Andrew Appel and Lennart Beringer and John Hatcliff and Xinming Ou and Andrew Cousino},
  title = 	 {A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow},
  booktitle =    {First conference on Principles of Security and Trust (part of ETAPS 2012)},
  editor = 	 {Pierpaolo Degano and Joshua Guttman},
  pages = 	 {369--389},
  series =       {LNCS},
  volume =       {7215}, 
  year = 	 {2012},
  publisher =    {Springer-Verlag},
}
 


Back to Main page



























@Article{ Amt+etal:IPL-2010,
  author = 	 {Torben Amtoft and Kelly Androutsopoulos and David Clark and Mark Harman and Zheng Li},
  title = 	 {An Alternative Characterization of Weak Order Dependence},
  journal = 	 {Information Processing Letters},
  year = 	 {2010},
  volume = 	 {110},
  pages = 	 {939--943},
  month = 	 OCT
} 
 


Back to Main page


























          
@InProceedings{,
  author = 	 {Torben Amtoft and John Hatcliff and Edwin Rodr\'{i}guez},
  title = 	 {Precise and Automated Contract-based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays},
  booktitle = {ESOP'10},
  pages = 	 {43--63},
  year = 	 {2010},
  editor = 	 {Andrew D. Gordon},
  volume = 	 {6012},
  series = 	 {LNCS},
  publisher =    {Springer}
}
 


Back to Main page


























 
@InProceedings{ ,
  author = 	 {Torben Amtoft and John Hatcliff and Edwin Rodriguez and Robby and Jonathan Hoag and David Greve},
  title = 	 {Specification and Checking of Software Contracts for Conditional Information Flow},
  booktitle =    {15th International Symposium on Formal Methods (FM'08)},
  year = 	 {2008},
  series = 	 {LNCS},
  volume =       {5014},
  pages =        {229--245},
  month = 	 MAY,
  publisher =    {Springer-Verlag},
  note = 	 {An extended version appears as Technical Report SAnToS-TR2007-5, CIS Department, Kansas State University, and later as chapter 12 in
Design and Verification of Microprocessor Systems for High-Assurance Applications, edited by David S. Hardin.}
}
 


Back to Main page



























@Article{ Amtoft:IPL-2007,
  author = 	 {Torben Amtoft},
  title = 	 {Slicing for Modern Program Structures:
a Theory for Eliminating Irrelevant Loops},
  journal = 	 {Information Processing Letters},
  year = 	 {2008},
  month =        APR,
  volume = 	 {106},
  number =       {2},
  pages = 	 {45--51},
  doi =          {http://dx.doi.org/10.1016/j.ipl.2007.10.002},
  note = 	 {An abridged version of Technical report 2007-3 
(with title: 'Correctness of Practical Slicing for Modern Program Structures'), 
Department of Computing and Information Sciences, Kansas State University, May 2007}
}
 


Back to Main page



























@InProceedings{,
  author = 	 {Torben Amtoft and Anindya Banerjee},
  title = 	 {Verification Condition Generation for Conditional Information Flow},
  booktitle = 	 {5th ACM Workshop on Formal Methods in Security Engineering (FMSE'07), George Mason University},
  pages = 	 {2--11},
  year = 	 {2007},
  OPTeditor = 	 {},
  month = 	 NOV,
  publisher =    {ACM},
  note = 	 {The full paper appears as Technical report 2007-2, Department of Computing and Information Sciences, Kansas State University, August 2007.}
}
 


Back to Main page



























@Article{,
  author = 	 {Torben Amtoft},
  title = 	 {Flow-Sensitive Type Systems and the Ambient Calculus},
  journal = 	 {Higher-Order and Symbolic Computation},
  year = 	 {2008},
  volume = 	 {21},
  number = 	 {4},
  pages = 	 {411--442},
  month = 	 DEC
}
 


Back to Main page



























@InProceedings{Amt+Ban+Ban:POPL-2006,
  author = 	 {Torben Amtoft and Sruthi Bandhakavi and Anindya Banerjee},
  title = 	 {A Logic for Information Flow in Object-Oriented Programs},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {The 33rd Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL'06)},
  pages = 	 {91--102},
  year = 	 {2006},
  editor = 	 {Simon Peyton Jones},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTorganization = {},
  publisher = {ACM Press},
  note = 	 {An extended version appears as Technical report CIS TR 2005-1, Department of Computing and Information Sciences, Kansas State University, July 2005}
}
 


Back to Main page



























@Article{Amt+Ban:SCP-2007,
  author = 	 {Torben Amtoft and Anindya Banerjee},
  title = 	 {A Logic for Information Flow Analysis with an Application to Forward Slicing of Simple Imperative Programs},
  journal = 	 {Science of Computer Programming}
  year = 	 {2007},
  volume = 	 {64},
  number =       {1},
  pages = 	 {3--28}
}
 


Back to Main page



























@Article{ 
  author = 	 {Venkatesh Prasad Ranganath and Torben Amtoft and Anindya Banerjee and John Hatcliff and Matthew B. Dwyer},
  title = 	 {A New Foundation for Control Dependence and Slicing for Modern Program Structures},
  journal = 	 TOPLAS,
  year = 	 {2007},
  volume = 	 {29},
  number = 	 {5},
  month = 	 AUG,
  note = 	 {Extended version of a paper appearing in the proceedings of ESOP 2005, pages 77--93, Springer LNCS 3444, April 2005.
A preliminary version appeared as Santos Technical report 2004-8, Department of Computing and Information Sciences, Kansas State University}
}



Back to Main page



























@InProceedings{,
  author = 	 {Torben Amtoft and Anindya Banerjee},
  title = 	 {Information Flow Analysis in Logical Form},
  booktitle = {SAS 2004 (11th Static Analysis Symposium), Verona, Italy, August 2004},
  pages =        {100--115},
  year = 	 {2004},
  editor = 	 {Roberto Giacobazzi},
  volume = 	 {3148},
  series = 	 {LNCS},
  publisher =    {Springer-Verlag},
  note = 	 {Awarded the SAS'04 Best Paper Award. The full paper appears as Technical report 2004-3, Department of Computing and Information Sciences, Kansas State University, April 2004.}
}
 


Back to Main page


























  
@InProceedings{,
  author = 	 {Torben Amtoft and Henning Makholm and J. B. Wells},
  title = 	 {PolyA: True Type Polymorphism for Mobile Ambients},
  booktitle = {TCS 2004 (3rd IFIP International Conference on Theoretical Computer Science), Toulouse, France, August 2004},
  pages = 	 {591--604},
  year = 	 {2004},
  editor = 	 {J.-J. Levy and E. W. Mayr and J. C. Mitchell},
  publisher = {Kluwer Academic Publishers},
  note = 	 {The full paper appears as Technical report HW-MACS-TR-0015, School of Mathematical and Computer Sciences, Heriot-Watt University, February 2004.}
}
 


Back to Main page



























@InProceedings{ Amt+Mul:TLDI-2003,
  author = 	 {Torben Amtoft and Robert Muller},
  title = 	 {Inferring Annotated Types for Inter-procedural Register Allocation with Constructor Flattening},
  booktitle =    {The 2003 ACM SIGPLAN international workshop on Types in Language Design and Implementation (TLDI'03)},
  location =     {New Orleans, Louisiana, USA},
  pages = 	 {86--97},
  year = 	 {2003},
  month =        JAN,
  series = 	 {SIGPLAN Notices},
  publisher = {ACM Press}
}
 


Back to Main page



























@Unpublished{,
  author = 	 {Torben Amtoft and J.B. Wells},
  title = 	 {Mobile Processes with Dependent Communication Types and Singleton Types for Names and Capabilities},
  note = 	 {Appears as Technical report 2002-3, Department of Computing and Information Sciences, Kansas State University},
  month = 	 OCT,
  year = 	 {2002},
}
 


Back to Main page



























@TechReport{
  author = 	 {Torben Amtoft},
  title = 	 {Causal Type System for Ambient Movements},
  institution =  {Department of Computing and Information Sciences, Kansas State University},
  year = 	 {2002},
  number = 	 {2002-04},
} 



Back to Main page



























@Article{,
  author = 	 {Torben Amtoft and Assaf J. Kfoury and Santiago M. Pericas-Geertsen},
  title = 	 {Orderly Communication in the Ambient Calculus},
  journal = 	 {Computer Languages},
  publisher =    {Elsevier Science},
  year = 	 {2002},
  volume = 	 {28},
  pages = 	 {29--60}
}
 


Back to Main page



























@InProceedings{ Amt+Kfo+Per:ESOP-2001,
  author = 	 {Torben Amtoft and Assaf J. Kfoury and Santiago M. Pericas-Geertsen},
  title = 	 {What are Polymorphically-Typed Ambients?},
  booktitle = 	 {ESOP 2001, Genova},
  pages = 	 {206--220},
  year = 	 {2001},
  editor = 	 {David Sands},
  volume = 	 {2028},
  series = 	 {LNCS},
  month = 	 APR,
  publisher =    {Springer-Verlag},
  note = 	 {The full paper appears as Boston University Technical Report BUCS-TR-2000-021, 2000.}
}
 


Back to Main page



























@InCollection{ Amt+Con+Dan+Mal:NDJ-2002,
  author = 	 {Torben Amtoft and Charles Consel and Olivier Danvy and Karoline Malmkj{\ae}r},
  title = 	 {The Abstraction and Instantiation of String-Matching Programs},
  booktitle = 	 {The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to {N}eil {D}. {J}ones},
  pages = 	 {332--357},
  publisher =    {Springer-Verlag},
  year = 	 {2002},
  editor = 	 {Torben Mogensen and David Schmidt and I. Hal Sudborough},
  volume = 	 {2566},
  series = 	 {Lecture Notes in Computer Science},
  note = 	 {An extended version appeared as Technical Report BRICS RS-01-12, DAIMI, Aarhus, Denmark, April 2001,}
}
 


Back to Main page



























@InProceedings{ Amt+Tur:ESOP-2000,
  author = 	 {Torben Amtoft and Franklyn Turbak},
  title = 	 {Faithful Translations between Polyvariant Flows and Polymorphic Types},
  booktitle = 	 {ESOP 2000, Berlin},
  pages = 	 {26--40},
  year = 	 {2000},
  volume = 	 {1782},
  series = 	 {LNCS},
  publisher =    {Springer-Verlag}
}
 


Back to Main page



























@TechReport{ ,
  author = 	 {Torben Amtoft},
  title = 	 {Partial Evaluation for Constraint-Based Program Analyses},
  institution =  {BRICS, Dept. of Computer Science, University of Aarhus},
  year = 	 {1999},
  number = 	 {BRICS-RS-99-45}
}
 


Back to Main page



























@Book{  ,
  author = 	 {Torben Amtoft and Flemming Nielson and Hanne Riis Nielson},
  title = 	 {Type and Effect Systems: Behaviours for Concurrency},
  publisher = 	 {Imperial College Press},
  year = 	 {1999},
  note =         {A very preliminary version, with the title {\em Polymorphic Subtyping for Side Effects}, appeared as 
Technical Report PB-529 from DAIMI, University of Aarhus, October 1997.}
}
 


Back to Main page



























@Article{        Amt+Nie+Nie:STTT-1998,
  author = 	 {Torben Amtoft and Hanne Riis Nielson and Flemming Nielson},
  title = 	 {Behaviour Analysis for Validating Communication Patterns},
  journal = 	 {Software Tools for Technology Transfer},
  year = 	 {1998},
  volume = 	 {2},
  number = 	 {1},
  pages = 	 {13--28},
  note = 	 {A preliminary version appeared as Technical Report PB-527 from DAIMI, University of Aarhus, September 1997.}
}
 


Back to Main page



























@InProceedings{  ,
  author = 	 {Hanne Riis Nielson and Torben Amtoft and Flemming Nielson},
  title = 	 {Behaviour Analysis and Safety Conditions: a Case Study in {CML}},
  booktitle = 	 {FASE'98 (part of ETAPS'98)},
  volume = 	 {1382},
  series = 	 {LNCS},
  year = 	 {1998},
  publisher =    {Springer-Verlag},
  pages = 	 {255--269},
  note = 	 {Also appeared as Technical Report PB-528 from DAIMI, University of Aarhus, October 1997.}
}
 


Back to Main page



























@InProceedings{  LOMAPS-DAIMI-14,
  author = 	 {Hanne Riis Nielson and Flemming Nielson and Torben Amtoft},
  title = 	 {Polymorphic Subtyping for Effect Analysis: the Static Semantics},
  booktitle = 	 {Analysis and Verification of Multiple-Agent Languages},
  volume = 	 {1192},
  series = 	 {LNCS},
  year = 	 {1997},
  publisher =    {Springer-Verlag},
  pages = 	 {141--171},
  note = 	 {A preliminary version appeared as Technical Report PB-501 from DAIMI, University of Aarhus, April 1996.}
}
 


Back to Main page



























@InProceedings{  LOMAPS-DAIMI-15,
  author = 	 {Torben Amtoft and Flemming Nielson and Hanne Riis Nielson and J{\"{u}}rgen Ammann},
  title = 	 {Polymorphic Subtyping for Effect Analysis: the Dynamic Semantics},
  booktitle = 	 {Analysis and Verification of Multiple-Agent Languages},
  volume = 	 {1192},
  series = 	 {LNCS},
  year = 	 {1997},
  publisher =    {Springer-Verlag},
  pages = 	 {172--206},
  note = 	 {A preliminary version appeared as Technical Report PB-502 from DAIMI, University of Aarhus, April 1996.}
}
 


Back to Main page



























@InProceedings{  LOMAPS-DAIMI-16,
  author = 	 {Flemming Nielson and Hanne Riis Nielson and Torben Amtoft},
  title = 	 {Polymorphic Subtyping for Effect Analysis: the Algorithm},
  booktitle = 	 {Analysis and Verification of Multiple-Agent Languages},
  OPTeditor = 	 {},
  volume = 	 {1192},
  series = 	 {LNCS},
  year = 	 {1997},
  publisher =    {Springer-Verlag},
  pages = 	 {207--243},
  note = 	 {A preliminary version appeared as Technical Report PB-503 from DAIMI, University of Aarhus, April 1996.}
}
 


Back to Main page



























@Article{        Amt+Nie+Nie:JFP-1997,
  author = 	 {Torben Amtoft and Flemming Nielson and Hanne Riis Nielson},
  title = 	 {Type and Behaviour Reconstruction for Higher-Order 
                  Concurrent Programs},
  journal = 	 {Journal of Functional Programming},
  year = 	 {1997},
  volume = 	 {7},
  number = 	 {3},
  month = 	 MAY,
  pages = 	 {321--347},
  note = 	 {Preliminary versions appeared as Technical Report PB-497 from DAIMI, University of Aarhus, November 1995, and in 
{\em Proceeding of the 6th Nordic Workshop on Programming Theory (NWPT'94)}, Uffe H. Engberg and Kim G. Larsen and Peter D. Mosses (ed.), BRICS Notes Series NS-94-6 pp. 80--95, 1994.}
}
 


Back to Main page



























@INPROCEEDINGS{ ,
  AUTHOR        = "Torben Amtoft",
  TITLE         = "Local Type Reconstruction by means of
   Symbolic Fixed Point Iteration",
  BOOKTITLE     = "ESOP '94:
   5th European Symposium on Programming, Edinburgh, U.K.",
  YEAR          = "1994",
  PUBLISHER     = "Springer-Verlag",
  SERIES        = "LNCS",
  VOLUME        = "788",
  PAGES         = "43--57"
}
 


Back to Main page



























@TECHREPORT{ ,
  AUTHOR        = "Torben Amtoft",
  TITLE         = "Strictness Types: An Inference Algorithm 
   and an Application",
  INSTITUTION   = "DAIMI, University of Aarhus, Denmark",
  YEAR          = "1993",
  MONTH         = AUG,
  NUMBER        = "PB-448"
}
 


Back to Main page



























@INPROCEEDINGS{ ,
  AUTHOR        = "Torben Amtoft",
  TITLE         = "Minimal Thunkification",
  BOOKTITLE     = "3rd International Workshop on Static Analysis
   (WSA '93), September 1993, Padova, Italy",
  YEAR          = "1993",
  PUBLISHER     = "Springer-Verlag",
  SERIES        = "LNCS",
  VOLUME        = "724",
  PAGES         = "218--229"
}
 


Back to Main page



























@PHDTHESIS{  ,
  AUTHOR        = "Torben Amtoft",
  TITLE         = "Sharing of Computations",
  SCHOOL        = "DAIMI, University of Aarhus, Denmark",
  YEAR          = "1993",
  NOTE          = "Technical report PB-453"
}
 


Back to Main page



























@INPROCEEDINGS{ ,
  AUTHOR        = "Torben Amtoft",
  TITLE         = "Unfold/fold Transformations Preserving 
   Termination Properties",
  BOOKTITLE     = "4th International Symposium on 
   Programming Language Implementation and Logic Programming 
   (PLILP '92), Leuven, Belgium",
  YEAR          = "1992",
  EDITOR        = "M. Bruynooghe and M. Wirsing",
  MONTH         = AUG,
  PUBLISHER     = "Springer-Verlag",
  SERIES        = "LNCS",
  VOLUME        = "631",
  PAGES         = "187--201"
}
 


Back to Main page



























@INPROCEEDINGS{ ,
  AUTHOR        = "Torben Amtoft",
  TITLE         = "Properties of Unfolding-based Meta-level Systems",
  BOOKTITLE     = "Partial Evaluation and Semantics-Based 
   Program Manipulation (PEPM '91), New Haven, Connecticut.",
  SERIES        = "Sigplan Notices",
  VOLUME        = "26",
  NUMBER        = "9",
  PAGES         = "243--254",
  YEAR          = "1991"
}
 


Back to Main page



























@ARTICLE{ ,
  AUTHOR        = "Torben Amtoft and Jesper Larsson Tr{\"{a}}ff",
  TITLE         = "Partial Memoization for obtaining Linear Time
   Behavior of a {2DPDA}",
  JOURNAL       = "Theoretical Computer Science",
  YEAR          = "1992",
  VOLUME        = "98",
  NUMBER        = "2",
  PAGES         = "347--356",
  MONTH         = MAY
}
 


Back to Main page



























@INPROCEEDINGS{  ,
  AUTHOR        = "Torben Amtoft and Thomas Nikolajsen and
   Jesper Larsson Tr{\"{a}}ff and Neil D. Jones",
  TITLE         = "Experiments with Implementations of 
   Two Theoretical Constructions",
  BOOKTITLE     = "Logic at Botik, USSR",
  YEAR          = "1989",
  PUBLISHER     = "Springer-Verlag",
  SERIES        = "LNCS",
  VOLUME        = "363",
  PAGES         = "119--133",
  MONTH         = JUL
}
 


Back to Main page



























@MASTERSTHESIS{ ,
  AUTHOR        = "Torben Amtoft and Jesper Larsson Tr{\"{a}}ff",
  TITLE         = "Memoization and its use in Lazy and Incremental
   Program Generation",
  SCHOOL        = DIKU,
  YEAR          = "1989",
  MONTH         = AUG,
  NOTE          = "No.\ 89-8-1"
}
 


Back to Main page