Department of Information Technology

UPMARC Seminars

Coming seminars

Date Time Room Speaker Topic
2016-11-30 15:15 ITC 1212 Prof. Peter Sewell, Cambridge University The semantics of a real machine instruction?
What is it?

(TAS)@UpMARC is a seminar serie on various topics related to UPMARC. It used to be held every Thursday Afternoon (hence, the name), but this constraint has somewhat been loosen with time. It is now renamed to Theory and Applications.


The purpose is to meet and learn what people in related areas are doing. It is necessary for any researcher to make presentations, and this is a great opportunity to train your presentation skills in a context that is more relaxed than a big conference. Your colleagues want to know what you are doing.


Scope: Presentations may give a broad overview of the person's research area, or go into details on some specific topic the speaker has worked on. The presentations should be accessible to anyone who is at least a PhD student in computer science without reading any related research papers.


PhD course credits: Indeed, you can get some for a presentation. (disclaimer )


It historically started as TAPVES and got extended to UPMARC.

How does it work?

Anyone is welcome to present and attend, including PhD students, senior researchers, and undergraduate students near finishing.

You can sign up to present on a (TAS)@UpMarc! Simply:

  • send an email to Jari Stenman with as much details about the presentation as possible. (Date, title, co-authors, slides, abstract, etc ...)

Or do it yourself:

  1. edit this wiki page and LäsIT or send a mail to lesit@it.uu.se with the headings of a normal LäsIT seminar.
  2. add your name
  3. [Optional] create a subpage called yyyy-mm-dd for your abstract and link it to your title
  4. Send an email to Jari Stenman to tell him you have done the ground work.

Previous seminars

Date Time Room Speaker Topic
2016-04-22 10:15 ITC 1145 Magnus Myreen (Chalmers) The CakeML project and its new verified compiler
2016-02-18 14:15 ITC 1145 Rumyana Neykova (Imperial College London) Verify me if you can: Supervisors, Actors and Session Types
2016-02-16 10:00 ITC 1146 Peter Hsu, Oracle Labs The CAVA 1 Computer: Exceptional Parallelism and Energy Efficiency
Wednesday, 2015-11-04 14:15 1112 Peter Schrammel, Oxford Synthesising Interprocedural Bit-Precise Termination Proofs
Wednesday, 2015-11-11 13:15 1145 Jakob Nordström, KTH A Survey of Proof Complexity from a SAT Solving Perspective
Thursday, 2015-11-12 15:15 2446 Dimitrios Kouzapas, University of Glasgow Mungo: Typechecking Protocols
Date Title Speaker
2015-08-14 Strings and Automata Modulo Theories Margus Veanes, Microsoft Research Redmond
2015-06-16 Thomas Wahl, Northeastern University Behavioral Non-Portability in Scientific Numeric Computing
2015-04-07 Composing task-based codes on heterogeneous architectures Andra Hugo
Wednesday, 2014-12-10 Approximations for Model Construction Aleksandar Zeljic, Uppsala University
Tuesday, 2014-11-04 Probabilistic Termination Holger Hermanns, University of Saarland, Germany
Wednesday, 2014-09-24 Generating Bounded Languages using Bounded Control Sets Radu Iosif
Monday, 2014-09-15 Automating Regression Verification Mattias Ulbrich
Wednesday, 2014-06-11 Verifying eventual consistency of optimistic replication systems Ahmed Bouajjani
Wednesday, 2014-06-11 Optimal Dynamic Partial Order Reduction Bengt Jonsson
Wednesday, 2014-06-11 Fully Automated Shape Analysis Based on Forest Automata Ondrej Lengal
Wednesday, 2014-06-11 Energy games, branching VASS and simulation preorder; an overview Richard Mayr
Wednesday, 2014-06-11 Adjacent ordered Multi pushdown systems Prakash Saivasan
Wednesday, 2014-06-11 Controllers for the verification of communicating multi-pushdown systems Aiswarya Cyriac
Wednesday, 2014-06-11 A linear-time algorithm for the orbit problem over cyclic groups Anthony Widjaja Lin
Wednesday, 2014-06-11 An Integrated Specification and Verification Technique for Highly Concurrent Data Structure Lukas Holik
Wednesday, 2014-06-11 String Constraints for Verification Jari Stenman
Thursday, 2014-03-13 Scaling online social network crawling and microblogging systems Xiaoming Fu, University of Göttingen
Tuesday, 2014-02-18 Online Social Networks For The People, By The People David Koll, University of Göttingen
Friday, 2013-11-15 Disciplined Approximate Computing: From Language to Hardware, and Beyond Luis Ceze, University of Washington
Tuesday, 2013-09-10 Better Coarse-Grained than Fine-Grained: Rating Network Paths for Locality-Aware Overlay Construction and Routing Wei Du, University of Goettingen, Germany
Monday, 2013-09-16 21st Century Computer Architecture Mark D. Hill, University of Wisconsin
Tuesday, 2013-09-24 Improving the efficiency of multicores in data centers Jason Mars, University of Michigan
Tuesday, 2013-06-18 Modelyze: Embedding DSLs for Modeling and Analyzing Cyber-Physical Systems David Broman
Tuesday, 2013-06-04 Power is Money: Spend it wisely -- Scalable Cores and Caches for Power-Constrained CMPs David Wood, University of Wisconsin
Tuesday, 2013-06-04 Reliable and Energy-Efficient Data Collection in Wireless Sensor Networks Feng Wang, University of Mississippi
Tuesday, 2013-05-28 Machine code, formal verification and functional programming Magnus Myreen, Univ. of Cambridge
Thursday, 2013-05-23 An Integrated Specification and Verification Technique for Highly Concurrent Data Structures Frédéric Haziza
Tuesday, 2013-05-21 An epistemic calculus for spatially distributed systems with potential applications to social networks Sophia Knight
Monday, 2013-05-20 Power-Aware Resource Management for LTE Base Stations Magnus Själander
Monday, 2013-05-20 Improving Processor Efficiency by Statically Pipelining Instructions David Whalley
Thursday, 2013-05-16 All for the price of few Frédéric Haziza
Wednesday, 2013-05-15 Choreography-driven programming Fabrizio Montesi
Tuesday, 2013-05-14 Learning in Graphical Congestion Games with Applications to Content Replication and Caching György Dán, Associate Professor, KTH
Wednesday, 2013-05-08 Model checking of data word Aiswarya Cyriac
Thursday, 2013-04-18 Automata Learning for Register Automata Sofia Cassel
Thursday, 2013-04-11 Symbolic Model Checking in Multi-formalism Modelling Environments Kai Lampka
Thursday, 2013-03-14 Temporal Logics on Words with Multiple Data Values Ahmet Kara, TU Dortmund
Tuesday, 2013-02-21 Automata Minimization and Language Inclusion Checking Richard Mayr
Monday, 2013-02-18 Sentential Decision Diagrams Adnan Darwiche, UCLA
Monday, 2013-02-11 Task Scheduling using Joelle's Effects Stephan Brandauer
Monday, 2013-01-28 Tracking information flow in web applications Andrei Sabelfeld, Chalmers
Friday, 2012-12-21 Ph.D. Thesis Defence David Eklöv
Friday, 2012-12-21 Lic. Thesis Defence Andreas Sembrant
Thursday, 2012-12-20 Portable, Scalable, per-Core Power Estimation for Intelligent Resource Management Sally McKee, Chalmers University
Thursday, 2012-12-20 Multi-Core Design and Optimization through Mechanistic Analytical Modeling Lieven Eeckhout, Ghent University
Thursday, 2012-12-20 Learning Cache Models by Measurements Jan Reineke, Saarland University
Monday, 2012-11-26 Evaluating the Accuracy of Annotations in the Loci 3.0 Pluggable Type Checker Nosheen Zaza
Thurssday, 2012-11-15 Checking Weak Simulation for One-Counter Nets Patrick Totzke, University of Edinburgh
Thursday, 2012-11-15 Licenciate Seminar: Extending Psi-calculi and their Formal Proofs Palle Raabjerg
Friday, 2012-11-09 Aspects of Value-Based and Strategic Software and Systems Engineering Research Anca-Juliana Stoica
Wednesday, 2012-11-07 Interpolation and Horn Clauses Hossein Hojjat, EPFL Lausanne
Thursday, 2012-10-25 Verification and Fence Insertion under the TSO Memory Model Carl Leonardsson
Thursday, 2012-10-18 Stream Programming for Distributed Systems Andrew Santosa, University of Sydney
Thursday, 2012-10-11 Nuclear Safety Needs Computer Science Research Pavel Krcal
Thursday, 2012-06-14 Understanding the Impact of Denial of Service Attacks on Virtual Machines Ryan Shea (Simon Fraser University, Canada)
Wednesday, 2012-05-30 Structured Aliasing Tobias Wrigstad
Wednesday, 2012-05-16 Charge! and Kopitiam
Efficient verification of Java-programs using higher-order separation logic in Coq.
Jesper Bengtson
Thursday, 2012-04-26 Test generation for LTE functionality Olga Grinchtein
Tuesday, 2012-04-24 Taming Past LTL and Flat Counter Systems Arnaud Sangnier, University Paris Diderot- Paris 7, France
Thursday, 2012-03-22 The pi-calculus: origin and recent developments Joachim Parrow
Thursday, 2012-03-01 Scheduling of mixed-criticality real-time systems Pontus Ekberg
Thursday, 2012-02-23 X-ray lasers and computational nightmares Prof. Janos Hajdu,
Laboratory of Molecular Biophysics,
Department of Cell and Molecular Biology
Thursday, 2012-02-09 ongoing work in probabilistic programming Johannes Borgström
Thursday, 2011-12-08 Analytics of Social Sensing Prof. Tarek Abdelzaher,
University of Illinois at Urbana Champaign
Tuesday, 2011-12-13 Encoding Synchrony Kirstin Peters
Thursday, 2011-12-01 Solving Scheduling Problems from High-Level Models Jean-Noël Monette
Thursday, 2011-11-24 Deciding Robustness against Total Store Ordering Roland Meyer
Thursday, 2011-11-10 Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata Ondrej Lengal
Thursday, 2011-10-27 Efficient Software-based Online Phase Classification Andreas Sembrant
Wednesday, 2011-10-05 Carrying Probabilistic Reasoning to the Infinite World: On the Verification of Infinite-State Markov Chains Parosh Abdulla
Thursday, 2011-09-29 A Succinct Canonical Register Automaton Model Sofia M. Cassel
Tuesday, 2011-09-20
and Thursday, 2011-09-22
Proving correctness of Java programs using higher order separation logic Jesper Bengtson
2011-09-14 1Integrating SAT, QBF and SMT Solvers with Interactive Theorem Provers Tjark Weber, Cambridge
Tuesday, 2011-08-23 Abstraction in Satisfiability Solvers Vijay D'Silva, Oxford University
Thursday, 2011-06-30 Pattern-based Verification for Multithreaded Programs Pierre Ganty, IMDEA Software Institute
Thursday, 2011-06-16 opaal: A Prototype Model Checker Mads Christian Olesen
Tuesday, 2011-06-14 The 1st Verified Software Competition: Experience Report Vladimir Klebanov, Karlsruhe Institute of Technology
Tuesday, 2011-05-31 Compositional Verification of Distributed Objects with Asynchronous Method Calls Wolfgang Ahrendt
Thursday, 2011-03-03 General Binding in Nominal Isabelle Christian Urban, TU Munich
Thursday, 2011-03-03 Hasse diagram Generators and Petri Nets Mateus de Oliveira Oliveira
Thursday, 2011-01-20 A Type and Effect System for Deadlock Avoidance in Low-level Languages Konstantinos Sagonas
Thursday, 2010-12-16 Semantic Subtyping with an SMT Solver Andrew D Gordon
Thursday, 2010-12-16 Code Rewriting Used for Thread-Modular Model Checking of Concurrent Programs Under TSO Carl Leonardsson
Thursday, 2010-12-09 Global Model Checking of Ordered Multi-Pushdown Systems Mohamed Faouzi Atig
Monday, 2010-11-29 Transactional Memory Then and Now Kevin Moore
Thursday, 2010-11-11 On Mereologies in Computing Science Dines Bjørner
Wednesday, 2010-10-27 Performance Measured by Timed Automata Jan Krcal
Thursday, 2010-10-14 A counter-example guided abstraction refinement scheme for parameterized verification Ahmed Rezine
Thursday, 2010-10-07 Collaborative Wireless Networks Björn Landfeldt
Tuesday, 2010-09-28 Diagrams and their role in mathematical proof Peter Chapman
Tuesday, 2010-09-28 Checking Roundoff Errors using Counterexample-Guided Narrowing Mizuhito Ogawa
Thursday, 2010-09-23 See the 2 topics Toshiaki Aoki
Tuesday, 2010-09-21 A Verified and Executable SLR parser generator in HOL4 Aditi Barthwal
Friday, 2010-08-20 On the Formal Foundation of a Verification Approach for System-Level Concurrent Programs Matthias Daum
Thursday, 2010-06-10 Techniques for Automata learning and their connection to conformance testing Bengt Jonsson
Thursday, 2010-06-10 Parameterized Verification of Ad Hoc Networks Arnaud Sangnier, Università di Genova, Italy
Monday, 2010-05-31 Rule Formats for Determinism and Idempotence Luca Aceto, Reykjavik University, Island
Thursday, 2010-05-27 Simple and Efficient Search Procedures for Combinatorial Optimization Serdar Kadioglu, Brown University, USA
Wednesday, 2010-05-19 Constraint-Based Testing Arnaud Gotlieb, INRIA Rennes, France
Wednesday, 2010-05-12 Recent Advances in Checking Sequence Construction Husnu Yenigun
Tuesday, 2010-05-04 Model checking epistemic logic Mika Cohen
Thursday, 2010-04-22 On the verification problem for weak memory models Mohamed-Faouzi Atig
Thursday 2010-03-18 When Simulation Meets Antichains (on Checking Language Inclusion of NFA) Yu-Fang Chen,
Academia Sinica, Taiwan
Wednesday 2010-03-10 Impact of Architecture and Technology for Extreme Scale on Software and Algorithm Design Jack Dongarra,
University of Tennessee, USA
Wednesday 2010-03-10 Controlled Data and Resource Sharing in Multi-Core Platforms Sandhya Dwarkadas,
University of Rochester, NY, USA
Thursday 2010-02-25 Loci: Pluggable Thread-Locality for Java-Like Languages Tobias Wrigstad
Wednesday 2010-02-17 Fast Adaptive Uniformization of the Chemical Master Equation Verena Wolf
Thursday 2010-02-11 Integrated virtualization: the silver bullet for future multi-core computing systems? Koen De Bosschere
Monday 2010-02-01 Automata for words and trees over infinite alphabet Henrik Björklund,
University of Umeå
Thursday 2009-12-03 Owicki-Gries, thread-modular model checking and Cartesian abstraction Alexander Malkis,
University of Freiburg
Monday 2009-11-30 A Compositional Theory for STM Haskell Johannes Borgström
Monday 2009-11-09 McErlang: a model checker for Erlang Clara Benac Earle,
Universidad Politécnica de Madrid
Thursday 2009-10-29 Introduction to OpenCL
and what you should know about the differences between GPUs and CPUs
David Black-Schaffer
Wednesday 2009-10-21 Resource utilization in data intensive embedded systems Thomas Gustafsson, from Jonköping Univ/Linköping Univ
Tuesday 2009-10-20 Data-driven Sensor Network Macroprogramming using ATaG Animesh Pathak, from INRIA
2009-10-08 Static Detection of Race Conditions in Erlang Konstantinos Sagonas
2009-09-24 Coloring the caches for predictability on multicores Wang Yi
2009-09-17 Sensei-UU: a flexible wireless sensor network testbed supporting mobile nodes Olof Rensfelt
Wednesday
2009-09-02
Self-Aware Networks and Quality of Service Prof. Erol Gelenbe
from Imperial College London
2009-08-27 Wireless Sensor Network security - fighting hidden attackers Davor Sutic
2009-08-20 Ex-jobb presentation: Generating Models of Communication Protocols Fides Aarts & Johan Uijen
2009-06-04 UpMARC research and plans Erik Hagersten and Konstantinos Sagonas
2009-05-14 Wireless Sensor Networks Adam Dunkels
2009-05-07 Learning Minimal Separating DFA's for Compositional Verification Yu-Fang Chen
2009-04-23 On the Role of Autonomics in Emerging Computational Ecosystems
(in relation with TDB)
Manish Parashar
2009-04-23 Formalizing the Logic-Automaton Connection Stefan Berghofer
2009-03-26 No seminar this week. Come instead to the UpMarc inauguration
2009-03-20 Computation on Reconfigurable Platforms Brittle Tsoi
2009-03-12 Three holy grails of programming models Joachim Parrow
2008-12-11 On the complexity of model checking 1-counter machines Richard Mayr
2008-12-04 Software research challenges for Ericsson Andras Vajda,
Strategic Software Researcher, Ericsson Finland
2008-11-20 Defect Detection and Gradual Typing of Erlang Programs Konstantinos Sagonas
2008-11-13 Shape Analysis of Data-Dependent Programs Ran Ji
2008-11-06 Analyzing Concurrent Algorithms under Weak Memory Orderings Bengt Jonsson
2008-10-16 Adaptive Random Re-Routing for Differentiated QoS in Sensor Networks Edith Ngai
2008-10-02 Multicore software development and tools -- industry experience Jakob Engblom, VirtuTech AB

From TAPVES:

Date Title Speaker
2008-06-17 Shape analysis through monotonic abstraction Jonathan Mörndal
2008-06-12 New Schedulability Test Conditions for Non-preemptive Scheduling on Multiprocessor Platforms Guan Nan
2008-05-29 Parameterized Tree Systems Frédéric Haziza
2008-05-15 A framework for high-level descriptions of concurrent systems Joachim Parrow
2008-05-08 Model Checking of Concurrent programs on Relaxed Memory Models Bengt Jonsson
2008-04-17 Abstract Algebra and Program Theory Kim Solin
2008-04-16 Rewriting Systems with Data Ahmed Bouajjani
2008-04-16 Local Proofs for Global Properties Kedar Namjoshi
2008-04-16 What else is decidable about integer arrays? Tomas Vojnar
Wed 2008-04-09 Computational Linguistics Resarch in Uppsala Joakim Nivre m.fl
Tue 2008-04-08 Specification and Verification of Dynamic Topology Systems Bernd Westphal
2008-03-27 Regular Inference for State Machines using Domains with Equality Tests Therese Berg
2008-03-19 A Kleene-Schutzenberger Theorem for Weighted Timed Automata Karin Quaas
2008-03-13 Constraint Programming: A Programming Paradigm on the Rise Pierre Flener
2008-03-06 Using a parallel data stream management system to achieve higly-scalable trip grouping for collective transportation. Erik Zeitler
2008-02-21 R-automata Pavel Krcal
2008-02-14 A completeness proof for bisimulation in the pi-calculus using Isabelle Jesper Bengtson
2007-12-13 The Symbolic Applied Pi-calculus Magnus Johansson
2007-12-06 DYMO verification using graph grammars Oskar Wibling
2007-11-29 Model Checking Parameterized Systems Parosh Abdulla
2007-11-15 Use of (Application) Domain Theories in Applied Formal Methods Lars-Henrik Eriksson
2007-11-08 Industrilogik's formal metods process and tools Lars-Henrik Eriksson
2007-11-05 Hydra Flash Memory Solid State Disk Architecture Sang Lyul Min
2007-10-25 Validating QoS properties of Biomedical Sensor Networks Simon Tschirner
2007-10-18 Introduction to and Overview of the MODEX tool forSoftware Verification Bengt Jonsson
2007-10-11 Security types for F# Jesper Bengtson
2007-10-04 Coherence and Memory Ordering: a hardware perspective Erik Hagersten
2007-05-31 Mobility and Expressiveness: an introduction Björn Victor
2007-05-22 Static Analysis of Dynamic Communication Systems Jörg Bauer
2007-05-10 Proving Termination of Tree Manipulating Programs Tomas Vojnar
2007-05-03 Attack Trees for Threat Analysis and Risk Assessment Jonathan Mörndal
Fri. 2007-04-27 Towards the Engineering of Modular Software for Increased Predictability Michel Schellekens
2007-04-12 Automata-Based Techniques for the Verification of Programs with Linked Data Structures Ahmed Bouajjani, University of Paris 7
2007-03-15 The Good, The Bad, and the Random. Stochastic Games with Lossy Channels. Sven Sandberg
2007-03-08 Learning of Timed Systems Olga Grinchtein
2007-03-01 Compositional Representation of Simulink/Stateflow-Models in HLang Simon Tschirner
2007-02-22 Success Typings - type signatures from a dynamic point of view Tobias Lindahl
2007-02-15 Formalising the pi-calculus using nominal logic Jesper Bengtson
2007-02-08 Compositional Analysis of Timed Systems by Abstraction Leonid Mokrushin
2007-02-01 Timed Automata and Clock Difference Relations Pavel Krcal
Tue. 2006-12-12 Spatio-Temporal Verification of Mobile Real-Time Systems Andreas Schäfer, University of Oldenburg, Germany
2006-12-07 Partial Order Reduction for Model Checking of Real-Time Components John Håkansson
2006-11-30 No TAPVES this week, but there is a testing seminar at 13:15. The scope is similar. Note: (1) the time is different. (2) You are supposed to read the related article before the seminar.
2006-11-23 Eager Markov Chains Noomene Ben Henda
2006-11-16 Verifying liveness properties of parameterized systems Mayank Saksena
2006-11-09 Parametrized Systems, Simplifying safety Ahmed Rezine
2006-11-02 Limiting Behavior of Infinite-State Systems Sven Sandberg

Updated  2016-11-30 08:39:10 by Bengt Jonsson.