Formal Methods and Tools

Research output

Research output per year 1987 2005 2006 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020 2021 2022 2023 2024 2025

• 760 Conference contribution
• 334 Article
• 164 Report
• 96 Chapter
• 277 More
  • 80 Paper
  • 60 PhD Thesis - Research UT, graduation UT
  • 29 Book editing
  • 22 Preprint
  • 14 Conference article
  • 14 Working paper
  • 10 Editorial
  • 8 Book
  • 7 Abstract
  • 6 Foreword/postscript
  • 4 Digital or Visual Products
  • 3 Inaugural speech
  • 3 Poster
  • 3 Meeting Abstract
  • 3 Web publication/site
  • 3 PhD Thesis - Research external, graduation UT
  • 3 EngD Thesis
  • 2 PhD Thesis - Research UT, graduation external
  • 1 Other
  • 1 Comment/Letter to the editor
  • 1 Software

Research output per year

Research output per year

Search results

• 2019

  VerifyThis2018: A Program Verification Competition

  Huisman, M., Monahan, R., Müller, P., Paskevich, A. & Ernst, G., Jan 2019

  Research output: Book/Report › Report › Academic

  Open Access

  File

  • Verification 100%
  • Challenges 100%
  • Competition 100%
  • Program 100%
  • Software 100%
  142 Downloads (Pure)
• 2017

  Analysis and Verification of Pointer Programs

  Huisman, M., Noll, T. & Tatsuta, M., 2017, Tokyo, Japan: National Institute of Informatics. (NII Shonan Meeting Reports; no. 2017-14)

  Research output: Book/Report › Report › Academic

  Open Access

  File
  56 Downloads (Pure)

• A Verification Technique for Deterministic Parallel Programs (extended version)

  Darabi, S., Blom, S. & Huisman, M., 25 Feb 2017, Enschede: Centre for Telematics and Information Technology (CTIT). 19 p. (CTIT technical report; no. TR-CTIT-17-01)

  Research output: Book/Report › Report › Other research output

  File
  257 Downloads (Pure)

• Rare event simulation for dynamic fault trees

  Ruijters, E. J. J., Reijsbergen, D. P., de Boer, P.-T. & Stoelinga, M. I. A., 10 Mar 2017, Enschede: Centre for Telematics and Information Technology (CTIT). 14 p. (CTIT technical report series; no. TR-CTIT-17-02)

  Research output: Book/Report › Report › Other research output

  File

  • Event Simulation 100%
  • Fault Tree 100%
  • Rare Event 100%
  • Trees 100%
  • Simulation 40%
  7 Citations (Scopus)

  101 Downloads (Pure)

• VerifyThis 2017: A Program Verification Competition

  Huisman, M., Monahan, R., Müller, P., Mostowski, W. & Ulbrich, M., 2017, Karlsruhe: Karlsruhe Institute of Technology. (Karlsruhe Reports in Informatics; no. 2017-10)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Verification 100%
  • Challenges 100%
  • Competition 100%
  • Program 100%
  • Sweden 50%
  181 Downloads (Pure)
• 2016

  A Model-Driven Framework for Hardware-Software Co-design of Dataflow Applications (extended version)

  Ahmad, W., Yildiz, B. M., Rensink, A. & Stoelinga, M., Sept 2016, Enschede: Centre for Telematics and Information Technology (CTIT). 23 p. (CTIT Technical Report Series; no. TR-CTIT-16-09)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Models 100%
  • Extended Version 100%
  • Participatory Design 100%
  • Application 100%
  • Driven Framework 100%
  148 Downloads (Pure)

• Model checking and evaluating QoS of batteries in MPSoC dataflow applications via hybrid automata (extended version)

  Ahmad, W., Jongerden, M. R., Stoelinga, M. I. A. & van de Pol, J. C., 15 Apr 2016, Enschede: Centre for Telematics and Information Technology (CTIT). 33 p. (CTIT Technical Report Series; no. TR-CTIT-16-03)

  Research output: Book/Report › Report › Professional

  File

  • System Manufacturer 100%
  113 Downloads (Pure)

• VerifyThis 2016: A Program Verification Competition

  Huisman, M., Monahan, R., Müller, P. & Poll, E., Jun 2016, Enschede: Centre for Telematics and Information Technology (CTIT). 6 p. (CTIT Technical Report Series; no. TR-CTIT-16-07)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Competition 100%
  • Program 100%
  • installment 50%
  • Serials 20%
  • Netherlands 20%
  162 Downloads (Pure)
• 2015

  A Model-Derivation Framework for Timing Analysis of Java Software Systems

  Yildiz, B. M., Rensink, A., Bockisch, C. & Aksit, M., 30 Dec 2015, Enschede: Centre for Telematics and Information Technology (CTIT). 26 p. (CTIT Technical Report Series; no. TR-CTIT-15-08)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Models 100%
  • Timing Analysis 100%
  • Software Systems 100%
  • Software Verification 10%
  • Model Checking 10%
  154 Downloads (Pure)

• Green computing: power optimisation of VFI-based real-time multiprocessor dataflow applications (extended version)

  Ahmad, W., Holzenspies, P. K. F., Stoelinga, M. I. A. & van de Pol, J. C., 24 Jun 2015, Enschede: Centre for Telematics and Information Technology (CTIT). 32 p. (CTIT Technical Report Series; no. TR-CTIT-15-04)

  Research output: Book/Report › Report › Professional

  File
  172 Downloads (Pure)

• History-based Verification of Functional Behaviour of Concurrent Programs

  Blom, S., Huisman, M. & Zaharieva-Stojanovski, M., 9 Mar 2015, Enschede: Centre for Telematics and Information Technology (CTIT). 25 p. (CTIT Technical Report Series; no. TR-CTIT-15-02)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • History 100%
  • Behavior 100%
  • Concurrent Program 100%
  • Global History 100%
  • Process Algebra 50%
  15 Citations (Scopus)

  194 Downloads (Pure)
• 2014

  Fault Tree Analysis: A survey of the state-of-the-art in modeling, analysis and tools

  Ruijters, E. J. J. & Stoelinga, M. I. A., 2 Dec 2014, Enschede: Centre for Telematics and Information Technology (CTIT). 36 p. (CTIT Technical Report Series; no. TR-CTIT-14-14)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Survey 100%
  • Fault Tree 100%
  • Analysis Method 33%
  • Models 16%
  • Standards 16%
  3681 Downloads (Pure)

• Formal specification with JML

  Huisman, M., Ahrendt, W., Bruns, D. & Hentschel, M., 2014, Karlsruhe: Karlsruhe Institute of Technology. 51 p. (Karlsruhe Reports in Informatics; no. 2014-10)

  Research output: Book/Report › Report › Professional

  File

  • Software 100%
  • Formal Specification 100%
  • modeling language 50%
  • Starting Point 50%
  381 Downloads (Pure)

• Modelling and analysis of Markov reward automata (extended version)

  Guck, D., Timmer, M., Hatefi, H., Ruijters, E. J. J. & Stoelinga, M. I. A., 2014, Enschede: Centre for Telematics and Information Technology (CTIT). 35 p. (CTIT Technical Report Series; no. TR-CTIT-14-06)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Costs 100%
  • Mathematical Model 100%
  • Analysis 100%
  • Extended Version 100%
  • Automaton 100%
  64 Downloads (Pure)

• Resource-constrained optimal scheduling of SDF graphs via timed automata (extended version)

  Ahmad, W., de Groote, R., Holzenspies, P. K. F., Stoelinga, M. I. A. & van de Pol, J. C., 21 Jan 2014, Enschede, the Netherlands: Centre for Telematics and Information Technology (CTIT). 32 p. (CTIT technical reports; no. TR-CTIT-13-17)

  Research output: Book/Report › Report › Other research output

  File
  99 Downloads (Pure)

• Resource-constrained optimal scheduling of synchronous dataflow graphs via timed automata

  Ahmad, W., de Groote, R., Holzenspies, P. K. F., Stoelinga, M. I. A. & van de Pol, J. C., 21 Jan 2014, Enschede: Centre for Telematics and Information Technology (CTIT). 32 p. (CTIT Technical Report Series; no. TR-CTIT-13-17)

  Research output: Book/Report › Report › Professional

  File
  16 Citations (Scopus)

  362 Downloads (Pure)

• Towards Online and Transactional Relational Schema Transformations

  Wevers, L., Hofstra, M., Tammens, M., Huisman, M. & van Keulen, M., 3 Nov 2014, Enschede: Centre for Telematics and Information Technology (CTIT). 19 p. (CTIT Technical Report Series; no. TR-CTIT-14-10)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Transformations 100%
  • Relational Schema 100%
  • Database 33%
  • Standards 16%
  • Classes 16%
  96 Downloads (Pure)

• Verifying Class Invariants in Concurrent Programs

  Zaharieva, M. & Huisman, M., 17 Jan 2014, Enschede: Centre for Telematics and Information Technology (CTIT). 20 p. (CTIT Technical Report Series; no. TR-CTIT-14-01)

  Research output: Book/Report › Report › Professional

  File
  4 Citations (Scopus)

  159 Downloads (Pure)
• 2013

  Confluence reduction for Markov automata (extended version)

  Timmer, M., van de Pol, J. & Stoelinga, M. I. A., Jun 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 26 p. (CTIT Technical Report Series; no. TR-CTIT-13-14)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Nondeterminism 100%
  77 Downloads (Pure)

• DFTCalc: a tool for efficient fault tree analysis (extended version)

  Arnold, F., Belinfante, A., van der Berg, F. I., Guck, D. & Stoelinga, M. I. A., Jun 2013, Enschede: Centre for Telematics and Information Technology (CTIT). (CTIT Technical Report Series; no. TR-CTIT-13-13)

  Research output: Book/Report › Report › Professional

  File

  • Extended Version 100%
  • Fault Tree 100%
  • Compression Technique 25%
  • Model Checking 25%
  • Risk Management 25%
  304 Downloads (Pure)

• Divergent Quiescent Transition Systems (extended version)

  Stokkink, W. G. J., Timmer, M. & Stoelinga, M. I. A., Mar 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 39 p. (CTIT Technical Report Series; no. TR-CTIT-13-08)

  Research output: Book/Report › Report › Academic

  Open Access

  File

  • Extended Version 100%
  • Transition System 100%
  • Models 100%
  • Automaton 80%
  • Behavior 50%
  45 Downloads (Pure)

• Formal specifications for Java’s synchronisation classes

  Amighi, A., Blom, S., Huisman, M., Mostowski, W. & Zaharieva-Stojanovski, M., 11 Sept 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 8 p. (CTIT Technical Report Series; no. TR-CTIT-13-18)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Synchronization 100%
  • Paper 18%
  • Approach 18%
  • Logic 18%
  • Primitive Operation 11%
  52 Downloads (Pure)

• Modelling, Reduction and Analysis of Markov Automata (extended version)

  Guck, D., Hatefi, H., Hermanns, H., Katoen, J. P. & Timmer, M., 30 May 2013, Ithaca, NY, USA: Cornell University. 27 p.

  Research output: Book/Report › Report › Academic

  File
  84 Downloads (Pure)

• On-the-fly confluence detection for statistical model checking (extended version)

  Hartmanns, A. & Timmer, M., Mar 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 18 p. (CTIT Technical Report Series; no. TR-CTIT-13-04)

  Research output: Book/Report › Report › Academic

  File

  • Extended Version 100%
  • Model Checking 100%
  • Detection 100%
  • Statistical Model 100%
  • Models 75%
  101 Downloads (Pure)

• Parallel transaction processing in functional languages, towards practical functional databases

  Wevers, L., Huisman, M. & de Keijzer, A., 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 16 p. (CTIT Technical Report Series; no. TR-CTIT-13-06)

  Research output: Book/Report › Report › Professional

  File
  56 Downloads (Pure)

• Publishing Your Prototype Tool on the Web: PUPTOL, a Framework

  Belinfante, A. & Rensink, A., Jun 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 8 p. (CTIT Technical Report Series; no. TR-CTIT-13-15)

  Research output: Book/Report › Report › Professional

  File
  82 Downloads (Pure)

• Quantitative penetration testing with item response theory (extended version)

  Arnold, F., Pieters, W. & Stoelinga, M. I. A., Oct 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 11 p. (CTIT Technical Report Series; no. TR-CTIT-13-20)

  Research output: Book/Report › Report › Professional

  File
  274 Downloads (Pure)

• Resource protection using atomics: patterns and verifications

  Amighi, A., Blom, S. & Huisman, M., 1 May 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 14 p. (CTIT Technical Report Series; no. TR-CTIT-13-10)

  Research output: Book/Report › Report › Professional

  File
  152 Downloads (Pure)

• Specification and verification of GPGPU programs

  Blom, S., Huisman, M. & Mihelcic, M., 8 Nov 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 18 p. (CTIT Technical Report Series; no. TR-CTIT-13-21)

  Research output: Book/Report › Report › Professional

  File
  105 Downloads (Pure)

• Specification and Verification of GPGPU programs using Permission-based Separation logic

  Huisman, M. & Mihelcic, M., Mar 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 8 p. (CTIT Technical Report Series; no. TR-CTIT-13-12)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Graphics Processing Unit 100%
  • Application 60%
  • Level Programming Language 20%
  • OpenCL 20%
  • Computing Power 20%
  80 Downloads (Pure)

• Witnessing the elimination of magic wands

  Blom, S. & Huisman, M., 8 Nov 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 22 p. (CTIT Technical Report Series; no. TR-CTIT-13-22)

  Research output: Book/Report › Report › Professional

  File
  229 Downloads (Pure)
• 2012

  Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification

  Ngo, M. T., Stoelinga, M. & Huisman, M., 12 Dec 2012, Enschede: Centre for Telematics and Information Technology (CTIT). 19 p. (CTIT Technical Report Series; no. TR-CTIT-13-01)

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Kripke Structure 100%
  • Data Protection 100%
  • Equal Probability 100%
  164 Downloads (Pure)

• Efficient Modelling and Generation of Markov Automata (extended version)

  Timmer, M., Katoen, J. P., van de Pol, J. C. & Stoelinga, M. I. A., 11 Jun 2012, Enschede: Centre for Telematics and Information Technology (CTIT). 35 p. (CTIT Technical Report Series; no. TR-CTIT-12-16)

  Research output: Book/Report › Report › Academic

  File
  84 Downloads (Pure)

• Generalised compositionality in graph transformation

  Ghamarian, A. H. & Rensink, A., 1 Jul 2012, Enschede: Centre for Telematics and Information Technology (CTIT). 21 p. (CTIT Technical Report Series; no. TR-CTIT-12-17)

  Research output: Book/Report › Report › Professional

  File
  4 Citations (Scopus)

  243 Downloads (Pure)

• Graph abstraction and abstract graph transformations (Amended version)

  Boneva, I. B., Kreiker, J., Kurban, M. E., Rensink, A. & Zambon, E., Oct 2012, Enschede: Centre for Telematics and Information Technology (CTIT). 54 p. (CTIT Technical Report Series; no. TR-CTIT-12-26)

  Research output: Book/Report › Report › Professional

  File
  117 Downloads (Pure)

• Graph Attribution Through Sub-Graphs

  Kastenberg, H. & Rensink, A., Nov 2012, Enschede: Centre for Telematics and Information Technology (CTIT). 24 p. (CTIT Technical Report Series; no. TR-CTIT-12-27)

  Research output: Book/Report › Report › Professional

  File
  166 Downloads (Pure)

• Graph Passing in Graph Transformation

  Ghamarian, A. H. & Rensink, A., 31 Jan 2012, Enschede: Centre for Telematics and Information Technology (CTIT). 18 p. (CTIT Technical Report Series; no. TR-CTIT-12-04)

  Research output: Book/Report › Report › Professional

  File
  94 Downloads (Pure)

• Talking quiescence: a rigorous theory that supports parallel composition, action hiding and determinisation (extended version)

  Stokkink, G., Timmer, M. & Stoelinga, M., 1 Feb 2012, Enschede: Centre for Telematics and Information Technology (CTIT). 25 p. (CTIT Technical Report Series; no. TR-CTIT-12-05)

  Research output: Book/Report › Report › Academic

  Open Access

  File

  • Extended Version 100%
  • Transition System 100%
  • Parallel Composition 100%
  • Transitions 37%
  • Input/Output 37%
  49 Downloads (Pure)
• 2011

  D-SAR: A Distributed Scheduling Algorithm for Real-time, Closed-Loop Control in Industrial Wireless Sensor and Actuator Networks

  Zand, P., Chatterjea, S., Ketema, J. & Havinga, P. J. M., 21 Mar 2011, Enschede: Centre for Telematics and Information Technology (CTIT). 8 p. (CTIT Technical Report Series; no. TR-CTIT-11-09)

  Research output: Book/Report › Report › Professional

  File
  126 Downloads (Pure)

• Formal Semantics of the CHART Transformation Language

  de Mol, M. J. & Rensink, A., Dec 2011, Enschede: Centre for Telematics and Information Technology (CTIT). (CTIT Technical Report Series; no. TR-CTIT-12-03)

  Research output: Book/Report › Report › Professional

  File
  63 Downloads (Pure)

• Parallel Recursive State Compression for Free

  Laarman, A., van de Pol, J. C. & Weber, M., 15 Apr 2011, Ithaca, NY: ArXiv.org. 19 p.

  Research output: Book/Report › Report › Professional

  File
  26 Citations (Scopus)

  76 Downloads (Pure)

• Scheduler-specific Confidentiality for Multi-Threaded Programs and Its Logic-Based Verification

  Huisman, M. & Ngo, M. T., 6 Oct 2011, Enschede: Centre for Telematics and Information Technology (CTIT). 21 p. (CTIT Technical Report Series; no. TR-CTIT-11-22)

  Research output: Book/Report › Report › Professional

  File
  189 Downloads (Pure)
• 2010

  A First Study of Compositionality in Graph Transformation

  Rensink, A., Feb 2010, Enschede: Centre for Telematics and Information Technology (CTIT). (CTIT Technical Report Series; no. TR-CTIT-10-08)

  Research output: Book/Report › Report › Professional

  File
  111 Downloads (Pure)

• A linear process-algebraic format for probabilistic systems with data (extended version)

  Katoen, J. P., van de Pol, J. C., Stoelinga, M. I. A. & Timmer, M., 7 Apr 2010, Enschede: Centre for Telematics and Information Technology (CTIT). 18 p. (CTIT Technical Report Series; no. TR-CTIT-10-11)

  Research output: Book/Report › Report › Academic

  File
  93 Downloads (Pure)

• Boosting Multi-Core Reachability Performance with Shared Hash Tables

  Laarman, A., van de Pol, J. & Weber, M., 16 Apr 2010, Ithaca, NY: ArXiv.org. 25 p.

  Research output: Book/Report › Report › Professional

  Open Access

  File

  • Hash Table 100%
  • Multicore 100%
  • Data Layout 20%
  • Data Structure 20%
  • Search Algorithm 20%
  62 Citations (Scopus)

  65 Downloads (Pure)

• Full Semantics Preservation in Model Transformation - A Comparison of Proof Techniques

  Hülsbusch, M., König, B., Rensink, A., Semenyak, M., Soltenborn, C. & Wehrheim, H., Feb 2010, Enschede: Centre for Telematics and Information Technology (CTIT). 33 p. (CTIT Technical Report Series; no. TR-CTIT-10-09)

  Research output: Book/Report › Report › Professional

  File
  229 Downloads (Pure)

• Isomorphism Checking for Symmetry Reduction

  Rensink, A., Apr 2010, Enschede: Centre for Telematics and Information Technology (CTIT). 15 p. (CTIT Technical Report Series; no. TR-CTIT-10-27)

  Research output: Book/Report › Report › Professional

  File
  109 Downloads (Pure)

• Modelling and Analysis Using GROOVE

  Ghamarian, A. H., de Mol, M. J., Rensink, A., Zambon, E. & Zimakova, M. V., Apr 2010, Enschede: Centre for Telematics and Information Technology (CTIT). 23 p. (CTIT Technical Report Series; no. TR-CTIT-10-18)

  Research output: Book/Report › Report › Professional

  File
  511 Downloads (Pure)

• Using Canonical Forms for Isomorphism Reduction in Graph-based Model Checking

  Kant, G., Jul 2010, Enschede: Centre for Telematics and Information Technology (CTIT). 34 p. (CTIT Technical Report Series; no. TR-CTIT-10-28)

  Research output: Book/Report › Report › Professional

  File
  380 Downloads (Pure)
• 2009

  A GROOVE Solution for the BPMN to BPEL Model Transformation

  de Mol, M. J. & Zimakova, M. V., Aug 2009, Enschede: Centre for Telematics and Information Technology (CTIT). 34 p. (CTIT Technical Report Series; no. TR-CTIT-09-31)

  Research output: Book/Report › Report › Professional

  File
  91 Downloads (Pure)