Research Output 2008 2018

Filter
Report
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: ScientificReport

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: Other research outputReport

Chemical analysis
Fusion reactions
Semantics

VerifyThis 2017: A Program Verification Competition

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

Research output: ProfessionalReport

competition
Sweden
conference
theory
program
2016

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: ProfessionalReport

competition
Netherlands
conference
theory
program
2015
6 Citations

History-based Verification of Functional Behaviour of Concurrent Programs

Blom, S., Huisman, M. & Zaharieva, 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: ProfessionalReport

Algebra
Specifications
2014

Formal specification with JML

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

Research output: ProfessionalReport

Specifications
Formal specification
Modeling languages

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: ProfessionalReport

Experiments
2 Citations

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: ProfessionalReport

Semantics
2013

Correct and Efficient Accelerator Programming (Dagstuhl Seminar 13142)

Cohen, A., Donaldson, A. F., Huisman, M. & Katoen, J. P. 2013 Dagstuhl, Germany: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. 17 p.

Research output: ScientificReport

Technical presentations
Particle accelerators
Computer science

Formal specifications for Java’s synchronisation classes

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

Research output: ProfessionalReport

Synchronization
Application programming interfaces (API)
Semantics
Specifications

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: ProfessionalReport

Resource allocation
Managers
Experiments

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: ProfessionalReport

Synchronization
Specifications
Data structures

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: ProfessionalReport

Computer programming languages
Energy efficiency

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: ProfessionalReport

Computer programming languages
Energy efficiency

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: ProfessionalReport

Separation logic
Encoding
Resources
Java
Specification
2012

Confidentiality for Probabilistic Multi-Threaded Programs and Its Verification

Ngo, M. T., Stoelinga, M. I. A. & 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: ProfessionalReport

Data privacy
2011

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: ProfessionalReport

Temporal logic
Model checking
Scheduling
Chemical analysis