Zobrazeno 1 - 10 of 107 pro vyhledávání: '"FMT-MC: MODEL CHECKING"'
1
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
2
Guard-based partial-order reduction
Autor: Alfons Laarman, Henri Hansen, Elwin Pater, Jaco van de Pol
Publikováno v: International journal on software tools for technology transfer, 18(4), 427-448. Springer
This paper aims at making partial-order reduction independent of the modeling language. To this end, we present a guard-based method which is a general-purpose implementation of the stubborn set method. We approach the implementation through so-calle
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::41796ed1b0d99a2eb1c85e7ecb0b012d
https://doi.org/10.1007/s10009-014-0363-9
Zobrazit plný text záznamu
3
Generating and Solving Symbolic Parity Games
Autor: Gijs Kant, Jaco van de Pol
Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 159, Iss Proc. GRAPHITE 2014, Pp 2-14 (2014)
Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014), 2-14
STARTPAGE=2;ENDPAGE=14;TITLE=Proceedings 3rd Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2014)
GRAPHITE
We present a new tool for verification of modal mu-calculus formulae for process specifications, based on symbolic parity games. It enhances an existing method, that first encodes the problem to a Parameterised Boolean Equation System (PBES) and then
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7eedf2a34fc7091e54cec9e58820d61e
https://doaj.org/article/06d20bc167874b6687632c6ebdfed416
Zobrazit plný text záznamu
4
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
5
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
6
Multi-Core Reachability for Timed Automata
Autor: Dalsgaard, Andreas, Laarman, Alfons, Larsen, Kim G., Olesen, Mads Chr., van de Pol, Jaco, Jurdziński, Marcin, Ničković, Dejan
Publikováno v: Formal Modeling and Analysis of Timed Systems: 10th International Conference, FORMATS 2012, London, UK, September 18-20, 2012, Proceedings, 91-106
STARTPAGE=91;ENDPAGE=106;TITLE=Formal Modeling and Analysis of Timed Systems
Lecture Notes in Computer Science ISBN: 9783642333644
FORMATS
Model checking of timed automata is a widely used technique. But in order to take advantage of modern hardware, the algorithms need to be parallelized. We present a multi-core reachability algorithm for the more general class of well-structured trans
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::18844fe1ea565170097183acd4a7bf7f
https://doi.org/10.1007/978-3-642-33365-1_8
Zobrazit plný text záznamu
7
Efficient Instantiation of Parameterised Boolean Equation Systems to Parity Games
Autor: Kant, Gijs, van de Pol, Jan Cornelis, Wijs, A.J., Bošnački, D., Edelkamp, S.
Publikováno v: Electronic Proceedings in Theoretical Computer Science, Vol 99, Iss Proc. GRAPHITE 2012, Pp 50-65 (2012)
GRAPHITE
First Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2012), 50-65
STARTPAGE=50;ENDPAGE=65;TITLE=First Workshop on GRAPH Inspection and Traversal Engineering (GRAPHITE 2012)
Parameterised Boolean Equation Systems (PBESs) are sequences of Boolean fixed point equations with data variables, used for, e.g., verification of modal mu-calculus formulae for process algebraic specifications with data. Solving a PBES is usually do
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::3c472fec44fd1aa31a87b0fa2e101716
https://doi.org/10.4204/eptcs.99.7
Zobrazit plný text záznamu
8
Multi-Core LTSmin: Marrying Modularity and Scalability
Autor: Laarman, Alfons, van de Pol, Jan Cornelis, Weber, M., Bobaru, Michaela, Havelund, Klaus, Holzmann, Gerard J., Joshi, Rajeev
Publikováno v: Lecture Notes in Computer Science ISBN: 9783642203978
NASA Formal Methods
Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011, 506-511
STARTPAGE=506;ENDPAGE=511;TITLE=Proceedings of the Third International Symposium on NASA Formal Methods, NFM 2011
The LTSmin toolset provides multiple generation and on-the-fly analysis algorithms for large graphs (state spaces), typically generated from concise behavioral specifications (models) of systems. LTSmin supports a variety of input languages, but its
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c610488c39cde9378ae9c8302857bbd9
https://doi.org/10.1007/978-3-642-20398-5_40
Zobrazit plný text záznamu
9
Distributed Branching Bisimulation Minimization by Inductive Signatures
Autor: Blom, Stefan, Brim, L., van de Pol, Jan Cornelis
Publikováno v: PDMC
Electronic Proceedings in Theoretical Computer Science, Vol 14, Iss Proc. PDMC 2009, Pp 32-46 (2009)
Proceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation, 32-46
STARTPAGE=32;ENDPAGE=46;TITLE=Proceedings 8th International Workshop on Parallel and Distributed Methods in verifiCation
We present a new distributed algorithm for state space minimization modulo branching bisimulation. Like its predecessor it uses signatures for refinement, but the refinement process and the signatures have been optimized to exploit the fact that the
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::48a12f0067f70f4d0ee27a32617bc0a8
https://doi.org/10.4204/eptcs.14.3
Zobrazit plný text záznamu
10
Synthesis and stochastic assessment of cost-optimal schedules
Autor: Holger Hermanns, Yaroslav S. Usenko, Johann L. Hurink, Henrik Bohnenkamp, Angelika Mader, David N. Jansen
Publikováno v: International journal on software tools for technology transfer, 12(5), 305-317. Springer
International Journal on Software Tools for Technology Transfer, 12, 305-318
International Journal on Software Tools for Technology Transfer, 12, 5, pp. 305-318
We treat the problem of generating cost-optimal schedules for orders with individual due dates and cost functions based on earliness/tardiness. Orders can run in parallel in a resource-constrained manufacturing environment, where resources are subjec
Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8daa76f226b462eeea3cb5131143fcc2
https://doi.org/10.1007/s10009-009-0129-y
Zobrazit plný text záznamu

Vyhledávací nástroje:

Upřesnit hledání

Omezení vyhledávání
Plný text Recenzováno Digitální knihovna AV ČR
Zdroje