Zobrazeno 1 - 10
of 13
pro vyhledávání: '"Flavio Lerda"'
Publikováno v:
ASE
The majority of the work carried out in the formal methods community throughout the last three decades has (for good reasons) been devoted to special languages designed to make it easier to experiment with mechanized formal methods such as theorem pr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1f15196b35f96393e652bff098004aa8
https://doi.org/10.1023/a:1022920129859
https://doi.org/10.1023/a:1022920129859
Autor:
Alexandre Donzé, James Kapinski, Edmund M. Clarke, Flavio Lerda, Bruce H. Krogh, Hitashyam Maka
Publikováno v:
AIAA Guidance, Navigation and Control Conference and Exhibit.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::16d11df619f519733c57e9c1c0c27bd3
https://doi.org/10.2514/6.2008-6800
https://doi.org/10.2514/6.2008-6800
Publikováno v:
Hybrid Systems: Computation and Control ISBN: 9783540789284
HSCC
HSCC
This paper describes an approach for bounded-time verification of safety properties of supervisory control software interacting with a continuous-time plant. A combination of software Model Checking and numerical simulation is used to compute a conse
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::d345786b28f199cfa5e48e032c8fc1f5
https://doi.org/10.1007/978-3-540-78929-1_25
https://doi.org/10.1007/978-3-540-78929-1_25
Publikováno v:
ACC
Model checkers for program verification have enjoyed considerable success in recent years. In the control systems domain, however, they suffer from an inability to account for the physical environment. For control systems, simulation is the most wide
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0b46503b1f88bb546eec6a1f1e11735e
https://doi.org/10.1109/acc.2008.4586906
https://doi.org/10.1109/acc.2008.4586906
Publikováno v:
CDC
This paper extends a method for integrating source-code model checking with dynamic system analysis to verify properties of controllers for nonlinear dynamic systems. Source-code model checking verifies the correctness of control systems including fe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7514377f2ba9a8e133ebb751b2e03d84
https://doi.org/10.1109/cdc.2008.4739247
https://doi.org/10.1109/cdc.2008.4739247
Publikováno v:
Next Generation Design and Verification Methodologies for Distributed Embedded Control Systems ISBN: 9781402062537
In real-time systems, correctness depends on the time at which events occur. Examples of real-time systems include timed protocols and many embedded system controllers. Timed automata are an extension of finite-state automata that include real-valued
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::27c7f4d2624082672ff8af61479f292c
https://doi.org/10.1007/978-1-4020-6254-4_1
https://doi.org/10.1007/978-1-4020-6254-4_1
Publikováno v:
POPL
This paper presents a procedure for the verification of multi-process systems based on considering a series of underapproximated models. The procedure checks models with an increasing set of allowed interleavings of the given set of processes, starti
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::130cf055bcfad2cf411dade731ea7325
https://doi.org/10.1145/1040305.1040316
https://doi.org/10.1145/1040305.1040316
Publikováno v:
Computer Aided Verification ISBN: 9783540223429
CAV
Scopus-Elsevier
CAV
Scopus-Elsevier
The counterexamples produced by model checkers are often lengthy and difficult to understand. In practical verification, showing the existence of a (potential) bug is not enough: the error must be understood, determined to not be a result of faulty s
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c9ebdb421a2b447886afa86efb75f35c
https://doi.org/10.1007/978-3-540-27813-9_35
https://doi.org/10.1007/978-3-540-27813-9_35
Publikováno v:
Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783540212997
TACAS
TACAS
We present a tool for the formal verification of ANSI-C programs using Bounded Model Checking (BMC). The emphasis is on usability: the tool supports almost all ANSI-C language features, including pointer constructs, dynamic memory allocation, recursi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::ec0b67be34aed99339ec0f74cef5edcb
https://doi.org/10.1007/978-3-540-24730-2_15
https://doi.org/10.1007/978-3-540-24730-2_15
Autor:
Flavio Lerda, Dimitra Giannakopoulou
Publikováno v:
Formal Techniques for Networked and Distributed Sytems — FORTE 2002 ISBN: 9783540001416
FORTE
FORTE
Model checking is an automated technique for checking that a system satisfies a set of required properties. With explicit-state model checkers, properties are typically defined in linear-time temporal logic (LTL), and are translated into Buchi automa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3d2d167d64dab654b9b4cf1e81d6a1f1
https://doi.org/10.1007/3-540-36135-9_20
https://doi.org/10.1007/3-540-36135-9_20