Publications

Sort by: Date | Author | Title

Sieczkowski, F., Bizjak, A. & Birkedal, L. (2015). ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages. In C. Urban & X. Zhang (Eds.), Interactive Theorem Proving: 6th International Conference, ITP 2015, Nanjing, China, August 24-27, 2015, Proceedings (pp. 375-390). Springer. https://doi.org/10.1007/978-3-319-22102-1_25

Clouston, R., Bizjak, A., Grathwohl, H. B. & Birkedal, L. (2015). Programming and reasoning with guarded recursion for coinductive types. In A. Pitts (Ed.), Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (pp. 305-316). Springer VS. https://doi.org/10.1007/978-3-662-46678-0_26

Midtgaard, J. & Møller, A. (2015). QuickChecking Static Analysis Properties. In 8th IEEE International Conference on Software Testing, Verification and Validation (ICST), 2015 (pp. 1-10). IEEE. https://doi.org/10.1109/ICST.2015.7102603

Devriese, D., Piessens, F. & Birkedal, L. (2015). Reasoning about Object Capabilities with Logical Relations and Effect Parametricity: Technical Report including Proofs and Details. Association for Computing Machinery. http://cs.au.dk/~birke/papers/object-capabilities-tr.pdf

Møller, A. & Naik, M. (2015). SOAP'15: Proceedings of the 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis. In Proceedings of the 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis Association for Computing Machinery. http://dl.acm.org/citation.cfm?id=2771284

Jensen, C. S., Møller, A., Raychev, V., Dimitrov, D. & Vechev, M. (2015). Stateless Model Checking of Event-Driven Applications. In OOPSLA 2015 : Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (pp. 57-73). Association for Computing Machinery. https://doi.org/10.1145/2814270.2814282

Madsen, M. (2015). Static Analysis of Dynamic Languages. Department of Computer Science, Aarhus University.

Bizjak, A. & Birkedal, L. (2015). Step-indexed logical relations for probability. In A. Pitts (Ed.), Foundations of Software Science and Computation Structures: 18th International Conference, FOSSACS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings (pp. 279-294 ). Springer VS. https://doi.org/10.1007/978-3-662-46678-0_18

Adamsen, C. Q., Møller, A. & Mezzetti, G. (2015). Systematic Execution of Android Test Suites in Adverse Conditions. In Proceedings of the 2015 International Symposium on Software Testing and Analysis, ISSTA '15 (pp. 83-93 ). Association for Computing Machinery. https://doi.org/10.1145/2771783.2771786

Bizjak, A., Birkedal, L. & Miculan, M. (2014). A model of countable nondeterminism in guarded type theory. In G. Dowek (Ed.), Rewriting and Typed Lambda Calculi: Joint International Conference, RTA-TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings (pp. 108-123). Springer VS. https://doi.org/10.1007/978-3-319-08918-8_8

Møller, A. & Schwarz, M. R. (2014). Automated Detection of Client-State Manipulation Vulnerabilities. A C M Transactions on Software Engineering and Methodology, 23/4, Article 29. https://doi.org/10.1145/2531921

Feldthaus, A. & Møller, A. (2014). Checking Correctness of TypeScript Interfaces for JavaScript Libraries. In OOPSLA '14 Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages & Applications Association for Computing Machinery. https://doi.org/10.1145/2660193.2660215

Andreasen, E. & Møller, A. (2014). Determinacy in Static Analysis of jQuery. In A. Black & T. Millstein (Eds.), Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages & Applications, OOPSLA '14 (pp. 17-31 ). Association for Computing Machinery. https://doi.org/10.1145/2660193.2660214

Spitters, B., Vickers, S. & Wolters, S. (2014). Gelfand spectra in Grothendieck toposes using geometric mathematics. Electronic Proceedings in Theoretical Computer Science, EPTCS, 158, 77-107. https://doi.org/10.4204/EPTCS.158.7

Svendsen, K. & Birkedal, L. (2014). Impredicative concurrent abstract predicates. In Z. Shao (Ed.), Programming Languages and Systems: 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings (pp. 149-168 ). Springer. https://doi.org/10.1007/978-3-642-54833-8_9

Ernst, E., Møller, A., Schwarz, M. R. & Strocco, F. (2014). Managing Gradual Typing with Message-Safety in Dart. Paper presented at International Workshop on Foundations of Object-Oriented Languages , Portland, United States. http://homepages.ecs.vuw.ac.nz/~servetto/Fool2014/

Birkedal, L. (2014). Modular reasoning about concurrent higher-order imperative programs. Abstract from ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Diego, United States. https://doi.org/10.1145/2535838.2537849

Madsen, M. & Møller, A. (2014). Sparse Dataflow Analysis with Pointers and Reachability. In M. Müller-Olm & H. Seidl (Eds.), Static Analysis: 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings (pp. 201-218). Springer VS. https://doi.org/10.1007/978-3-319-10936-7_13

Madsen, M. & Andreasen, E. (2014). String Analysis for Dynamic Field Access. In A. Cohen (Ed.), Compiler Construction: 23rd International Conference, CC 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings (pp. 197-217). Springer. https://doi.org/10.1007/978-3-642-54807-9_12

Damgaard, T. C., Glenstrup, A. J., Birkedal, L. & Milner, R. (2013). An inductive characterization of matching in binding bigraphs. Formal Aspects of Computing, 25(2), 257-288. https://doi.org/10.1007/s00165-011-0184-5

Schwinghammer, J., Birkedal, L., Pottier, F., Reus, B., Støvring, K. & Yang, H. (2013). A step-indexed Kripke model of hidden state. Mathematical Structures in Computer Science, 23(1), 1-54. https://doi.org/10.1017/S0960129512000035

Jensen, C. S., Prasad, M. R. & Møller, A. (2013). Automated Testing with Targeted Event Sequence Generation. In M. Pezzè & M. Harman (Eds.), International Symposium on Software Testing and Analysis (ISSTA), 2013: Proceedings (pp. 67-77). Association for Computing Machinery. https://doi.org/10.1145/2483760.2483777

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Higher-order Concurrent Abstract Predicates.

Birkedal, L. & Mogelberg, R. E. (2013). Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. Annual Symposium on Logic in Computer Science, 213-222. https://doi.org/10.1109/LICS.2013.27

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Joins: A case study in modular specification of a concurrent reentrant higher-order library. In G. Castagna (Ed.), 27th European Conference on Object-Oriented Programming, ECOOP 2013; Montpellier; France (pp. 327-351). Springer. https://doi.org/10.1007/978-3-642-39038-8_14

Turon, A. J., Thamsborg, J., Ahmed, A., Birkedal, L. & Dreyer, D. (2013). Logical relations for fine-grained concurrency. In POPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (pp. 343-356). Association for Computing Machinery. https://doi.org/10.1145/2429069.2429111

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Modular Reasoning about Separation of Concurrent Data Structures. In M. Felleisen & P. Gardner (Eds.), Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (pp. 169-188 ). Springer. https://doi.org/10.1007/978-3-642-37036-6_11

Madsen, M., Livshits, B. & Fanning, M. (2013). Practical static analysis of JavaScript applications in the presence of frameworks and libraries. In B. Meyer, L. Baresi & M. Mezini (Eds.), Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering , ESEC/FSE 2013 (pp. 499-509). Association for Computing Machinery. https://doi.org/10.1145/2491411.2491417

Feldthaus, A. & Møller, A. (2013). Semi-Automatic Rename Refactoring for JavaScript. ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications, 323-338 . https://doi.org/10.1145/2509136.2509520

Jensen, C. S., Møller, A. & Su, Z. (2013). Server Interface Descriptions for Automated Testing of JavaScript Web Applications. In B. Meyer, L. Baresi & M. Mezini (Eds.), Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013 (pp. 510-520 ). Association for Computing Machinery. https://doi.org/10.1145/2491411.2491421

Birkedal, L., Bizjak, A. & Schwinghamme, J. (2013). Step-Indexed Relational Reasoning for Countable Nondeterminism. Logical Methods in Computer Science, 9(4), Article 4. https://doi.org/10.2168/LMCS-9(4:4)2013

Makarov, E. & Spitters, B. (2013). The Picard algorithm for ordinary differential equations in Coq. In Interactive Theorem Proving - 4th International Conference, ITP 2013, Proceedings (pp. 463-468) https://doi.org/10.1007/978-3-642-39634-2_34

Krebbers, R. & Spitters, B. (2013). Type classes for efficient exact real arithmetic in CoQ. Logical Methods in Computer Science, 9(1). https://doi.org/10.2168/LMCS-9(1:01)2013

Turon, A., Dreyer , D. & Birkedal, L. (2013). Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In G. Morrisett & T. Uustalu (Eds.), Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP '13 (pp. 377-390 ). Association for Computing Machinery. https://doi.org/10.1145/2500365.2500600

Svendsen, K., Birkedal, L. & Parkinson, M. (2013). Verification of the Joins Library in Higher-Order Separation Logic. http://www.itu.dk/people/kasv/joins-tr.pdf

Dinsdale-Young, T., Birkedal, L., Gardner, P., Parkinson, M. & Yang, H. (2013). Views: Compositional reasoning for concurrent programs. In R. Giacobazzi & R. Cousot (Eds.), POPL '13 Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages : Proceedings (pp. 287-299). Association for Computing Machinery. https://doi.org/10.1145/2429069.2429104

Birkedal, L., Sieczkowski, F. & Thamsborg, J. J. (2012). A Concurrent Logical Relation. In P. Cégielski & A. Durand (Eds.), Computer Science Logic 2012: 26th International Workshop. 21th Annual Conference of the EACSL. CSL’12, September 3–6, 2012, Fontainebleau, Franc Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.CSL.2012.107

Birkedal, L., Støvring, K. & Thamsborg, J. (2012). A relational realizability model for higher-order stateful. Journal of Logical and Algebraic Methods in Programming, 81(4), 491-521. http://ac.els-cdn.com.ez.statsbiblioteket.dk:2048/S1567832612000203/1-s2.0-S1567832612000203-main.pdf?_tid=fb853fd6-00fa-11e4-a19b-00000aab0f6b&acdnat=1404204049_088283a10b310a3f6cd3280168eb7093

Møller, A. & Schwarz, M. (2012). Automated Detection of Client-State Manipulation Vulnerabilities. In M. Glinz, G. Murphy & M. Pezzè (Eds.), 34th International Conference on Software Engineering (ICSE 2012) : Proceedings (pp. 749 - 759 ). IEEE Communications Society. https://doi.org/10.1109/ICSE.2012.6227143

Heunen, C., Landsman, N. P. & Spitters, B. (2012). Bohrification of operator algebras and quantum logic. Synthese, 186(3), 719-752. https://doi.org/10.1007/s11229-011-9918-4

Bengtson, J., Jensen, J. B. & Birkedal, L. (2012). Charge! A framework for higher-order separation logic in Coq. In L. Beringer & A. Felty (Eds.), Interactive Theorem Proving: Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings (Vol. 7406, pp. 315-331). Springer VS. https://doi.org/10.1007/978-3-642-32347-8_21

Jensen, J. B. & Birkedal, L. (2012). Fictional Separation Logic. In H. Seidl (Ed.), Lecture Notes in Computer Science: 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings (Vol. 7211, pp. 377-396). Springer.

Birkedal, L., Møgelberg, R. E., Schwinghammer, J. & Støvring, K. (2012). First steps in synthetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science, 8(4). https://doi.org/10.2168/LMCS-8(4:1)2012

Mehnert, H., Sieczkowski, F., Birkedal, L. & Sestoft, P. (2012). Formalized verification of snapshotable trees: Separation and sharing. In R. Joshi, P. Müller & A. Podelski (Eds.), Verified Software: Theories, Tools, Experiments: 4th International Conference, VSTTE 2012, Philadelphia, PA, USA, January 28-29, 2012. Proceedings (pp. 179-195). Springer. https://doi.org/10.1007/978-3-642-27705-4_15

Birkedal, L. (2012). Foundations of Software Science and Computational Structures: 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings. Springer. Lecture Notes in Computer Science Vol. 7213 https://doi.org/10.1007/978-3-642-28729-9

Andreasen, E., Feldthaus, A., Jensen, S. H., Jensen, C. S., Jonsson, P. A., Madsen, M. & Møller, A. (2012). Improving Tools for JavaScript Programmers (Position Paper). Paper presented at International Workshop on Scripts to Programs, Beijing, China. http://cs.au.dk/~amoeller/papers/stop/

Jensen, S. H., Jonsson, P. A. & Møller, A. (2012). Remedying the Eval that Men Do. In M. Heimdahl & Z. Su (Eds.), 2012 International Symposium on Software Testing and Analysis (ISSTA) : Proceedings (pp. 34-44). Association for Computing Machinery. https://doi.org/10.1145/2338965.2336758

Dreyer, D., Neis, G. & Birkedal, L. (2012). The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming, 22(4-5 special issue), 477-528. https://doi.org/10.1017/S0956796812000287

Spitters, B. (2012). The Space of Measurement Outcomes as a Spectral Invariant for Non-Commutative Algebras. Foundations of Physics, 42(7), 896-908. https://doi.org/10.1007/s10701-011-9619-3

Thamsborg, J. J., Birkedal, L. & Yang, H. (2012). Two for the Price of One: Lifting Separation Logic Assertions. Logical Methods in Computer Science, 8(3).

Displaying results 351 to 400 out of 545

Revised 05.12.2025

Marianne Dammand Iversen