Výsledky vyhledávání

RERS 2016

Autor: Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., van de Pol, Jan Cornelis, Margaria, T.

Publikováno v: Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II, 787-803
STARTPAGE=787;ENDPAGE=803;TITLE=Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications
Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications ISBN: 9783319471686
ISoLA (2)

The 5th challenge of Rigorous Examination of Reactive Systems (RERS 2016) once again provided generated and tailored benchmarks suited for comparing the effectiveness of automatic software verifiers. RERS is the only software verification challenge t

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::65f3d42c513d539456e4a9f138cfe2cc
https://doi.org/10.1007/978-3-319-47169-3_59

Zobrazit plný text záznamu

Verification of concurrent systems with VerCors

Autor: Amighi, Afshin, Blom, Stefan, Darabi, Saeed, Huisman, Marieke, Mostowski, Wojciech, Zaharieva-Stojanovski, Marina, Bernardo, Marco, Damiani, Ferruccio, Hähnle, Reiner, Broch Johnsen, Einar, Schaefer, Ina

Publikováno v: Formal Methods for Executable Software Models: 14th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, 172-216
STARTPAGE=172;ENDPAGE=216;TITLE=Formal Methods for Executable Software Models
Lecture Notes in Computer Science ISBN: 9783319073163
SFM

This paper presents the VerCors approach to verification of concurrent software. It first discusses why verification of concurrent software is important, but also challenging. Then it shows how within the VerCors project we use permission-based separ

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a0080b482db1aa0e7dab92acfd519511
https://doi.org/10.1007/978-3-319-07317-0_5

Zobrazit plný text záznamu

Multi-core Symbolic Bisimulation Minimisation

Autor: van Dijk, Tom, van de Pol, Jan Cornelis, Chechik, M., Raskin, J.-F.

Publikováno v: Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783662496732
TACAS
Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016), 332-348
STARTPAGE=332;ENDPAGE=348;TITLE=Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2016)

Bisimulation minimisation alleviates the exponential growth of transition systems in model checking by computing the smallest system that has the same behavior as the original system according to some notion of equivalence. One popular strategy to co

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8a54b4e9ca201b7b3f2e5d2a4f638d80
https://doi.org/10.1007/978-3-662-49674-9_19

Zobrazit plný text záznamu

Partial-order reduction for GPU model checking

Autor: Neele, T., Wijs, A., Bosnacki, D., van de Pol, Jan Cornelis, Artho, C, Legay, A., Peled, D.

Publikováno v: Automated Technology for Verification and Analysis-14th International Symposium, ATVA 2016, Proceedings, 357-374
STARTPAGE=357;ENDPAGE=374;TITLE=Automated Technology for Verification and Analysis-14th International Symposium, ATVA 2016, Proceedings
Automated Technology for Verification and Analysis ISBN: 9783319465197
ATVA
Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016, 357-374
STARTPAGE=357;ENDPAGE=374;TITLE=Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis, ATVA 2016

Model checking using GPUs has seen increased popularity over the last years. Because GPUs have a limited amount of memory, only small to medium-sized systems can be verified. For on-the-fly explicitstate model checking, we improve memory efficiency b

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::10de7e7a1e4f6589ac3efa9aa3089c8f
https://research.tue.nl/nl/publications/5423dd59-71b1-4e3f-8943-a5ef2a952a19

Zobrazit plný text záznamu

Preface

Publikováno v: Proceedings of the 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014). :1-3

This is a preface of the special issue of the 14th international workshop on Automated Verification of Critical Systems. This workshop covers all aspects of automated verification, including model checking, theorem proving, SAT/SMT constraint solving

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dris___00893::d2769fb6c717c706bdcec03e3bf70242
http://journal.ub.tu-berlin.de/eceasst/issue/view/84

Zobrazit plný text záznamu

A graph-based aspect interference detection approach for UML-based aspect-oriented models

Autor: Ciraci, Selim, Havinga, Wilke, Aksit, Mehmet, Bockisch, Christoph, van den Broek, Pim, Katz, Shmuel, Mezini, Mira, Kienzle, Jörg

Publikováno v: Transactions on Aspect-Oriented Software Development VII ISBN: 9783642160851
Transactions on Aspect-Oriented Software Development VII: A Common Case Study for Aspect-Oriented Modeling, 321-374
STARTPAGE=321;ENDPAGE=374;TITLE=Transactions on Aspect-Oriented Software Development VII

Aspect-Oriented Modeling (AOM) techniques facilitate separate modeling of concerns and allow for a more flexible composition of the resulting models than traditional techniques. While this improves the understandability of each submodel, in order to

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b83eae09051e24b8335edb5f00868c27
https://doi.org/10.1007/978-3-642-16086-8_9

Zobrazit plný text záznamu

Automated Verification of Nested DFS

Autor: van de Pol, Jan Cornelis, Núñez, M., Güdemann, M.

Publikováno v: Formal Methods for Industrial Critical Systems ISBN: 9783319194578
FMICS
Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015), 181-197
STARTPAGE=181;ENDPAGE=197;TITLE=Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2015)

In this paper we demonstrate the automated verification of the Nested Depth-First Search (NDFS) algorithm for detecting accepting cycles. The starting point is a recursive formulation of the NDFS algorithm. We use Dafny to annotate the algorithm with

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::096ba2d44a4c565be53220189ba6189e
https://doi.org/10.1007/978-3-319-19458-5_12

Zobrazit plný text záznamu

Preface

Autor: Huisman, Marieke, van de Pol, Jaco

Publikováno v: Proceedings of the 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014), 1-3
STARTPAGE=1;ENDPAGE=3;TITLE=Proceedings of the 14th International Workshop on Automated Verification of Critical Systems (AVoCS 2014)

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=narcis______::5b7451ba2805d69985c5aa660b99f4bd
https://research.utwente.nl/en/publications/preface(d5f78837-888b-44a0-bec7-b82f503b902d).html

Zobrazit plný text záznamu

Verifying Functional Behaviour of Concurrent Programs

Autor: Zaharieva, M., Huisman, Marieke, Blom, Stefan, Pearce, D.

Publikováno v: FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs, 4:1-4:6
STARTPAGE=4:1;ENDPAGE=4:6;TITLE=FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs
FTfJP@ECOOP

Specifying the functional behaviour of a concurrent program can often be quite troublesome: it is hard to provide a stable method contract that can not be invalidated by other threads. In this paper we propose a novel modular technique for specifying

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4b41d15e0117dc4821ddda1076e5df8a
https://research.utwente.nl/en/publications/c0081c37-6f29-4fa6-956c-b069c672f5f8

Zobrazit plný text záznamu

Verifying class invariants in concurrent programs

Autor: Zaharieva, M., Huisman, Marieke, Gnesi, Stefania, Rensink, Arend

Publikováno v: Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014), 230-245
STARTPAGE=230;ENDPAGE=245;TITLE=Proceedings of the 17th International Conference on Fundamental Approaches to Software Engineering (FASE 2014)
Fundamental Approaches to Software Engineering ISBN: 9783642548031
FASE

Class invariants are a highly useful feature for the verification of object-oriented programs, because they can be used to capture all valid object states. In a sequential program setting, the validity of class invariants is typically described in te

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7c98586d7a24c7d2cbbd34b42753ce2e
https://research.utwente.nl/en/publications/verifying-class-invariants-in-concurrent-programs(9714392c-ce7b-4556-ae46-fb20202c5de9).html

Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání