Zobrazeno 1 - 10
of 11
pro vyhledávání: '"Pascal Kesseli"'
Autor:
Alessandro Abate, Haniel Barbosa, Clark Barrett, Cristina David, Pascal Kesseli, Daniel Kroening, Elizabeth Polgreen, Andrew Reynolds, Cesare Tinelli
Publikováno v:
Abate, A, Barbosa, H, Barrett, C, David, C, Kesseli, P, Kroening, D, Polgreen, E, Reynolds, A & Tinelli, C 2023, ' Synthesising programs with non-trivial constants ', Journal of Automated Reasoning, vol. 67, no. 2, 19, pp. 1-25 . https://doi.org/10.1007/s10817-023-09664-4
Program synthesis is the mechanised construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. While useful
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::30b39fda6c7b58909962d5d926f0100d
https://www.pure.ed.ac.uk/ws/files/347664382/Synthesising_ABATE_DOA02032023_VOR_CC_BY.pdf
https://www.pure.ed.ac.uk/ws/files/347664382/Synthesising_ABATE_DOA02032023_VOR_CC_BY.pdf
Publikováno v:
Chockler, H, Kesseli, P, Kroening, D & Strichman, O 2020, ' Learning the Language of Software Errors ', Journal of Artificial Intelligence Research, vol. 67, pp. 881-903 . https://doi.org/10.1613/jair.1.11798
We propose to use algorithms for learning deterministic finite automata (DFA), such as Angluin’s L* algorithm, for learning a DFA that describes the possible scenarios under which a given program error occurs. The alphabet of this automaton is give
Autor:
Benjamin Maschler, Michael Weyrich, Pascal Kesseli, Dustin White, Philipp Marks, Matthias Weis
Publikováno v:
INDIN
Nowadays, formal methods are used in various areas for the verification of programs or for code generation from models in order to increase the quality of software and to reduce costs. However, there are still fields in which formal methods have not
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::28a7896999d6e286a2e21ad45bdddd88
Publikováno v:
FM 2016: Formal Methods ISBN: 9783319489889
Static analysers search for overapproximating proofs of safety commonly known as safety invariants. Conversely, static bug finders (e.g. Bounded Model Checking) give evidence for the failure of an assertion in the form of a counterexample trace. As o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8b86f5f00cf84d076bbc4bc7be698262
Autor:
Alessandro Abate, Lucas C. Cordeiro, Dario Cattaruzza, Daniel Kroening, Cristina David, Iury Bessa, Elizabeth Polgreen, Pascal Kesseli
Publikováno v:
Abate, A, Bessa, I, Cattaruzza, D, Cordeiro, L, David, C, Kesseli, P, Kroening, D & Polgreen, E 2017, Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants . in R Majumdar & V Kunčak (eds), Computer Aided Verification : 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I . Lecture Notes in Computer Science, no. 10426, Springer, Cham, pp. 462-482, 32nd IEEE/ACM International Conference on Automated Software Engineering, Urbana-Champaign, Illinois, United States, 30/10/17 . https://doi.org/10.1007/978-3-319-63387-9_23
Computer Aided Verification ISBN: 9783319633862
CAV (1)
Abate, A, Bessa, I, Cattaruzza, D, Cordeiro, L, David, C, Kesseli, P, Kroening, D & Polgreen, E 2017, ' Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants ', Lecture Notes in Computer Science . https://doi.org/10.1007/978-3-319-63387-9_23
Computer Aided Verification ISBN: 9783319633862
CAV (1)
Abate, A, Bessa, I, Cattaruzza, D, Cordeiro, L, David, C, Kesseli, P, Kroening, D & Polgreen, E 2017, ' Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants ', Lecture Notes in Computer Science . https://doi.org/10.1007/978-3-319-63387-9_23
We present a sound and automated approach to synthesize safe digital feedback controllers for physical plants represented as linear, time-invariant models. Models are given as dynamical equations with inputs, evolving over a continuous state space an
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ce975bfb7a1ab87139894f4d5095cc3f
Publikováno v:
Abate, A, David, C, Kesseli, P, Kroening, D & Polgreen, E 2018, Counterexample Guided Inductive Synthesis Modulo Theories . in H Chockler & G Weissenbacher (eds), Computer Aided Verification . Lecture Notes in Computer Science, vol. 10981, Springer Nature, pp. 270-288, International Conference on Computer Aided Verification, Oxford, United Kingdom, 14/07/18 . https://doi.org/10.1007/978-3-319-96145-3_15
Abate, A, David, C, Kesseli, P, Kroening, D & Polgreen, E 2018, Counterexample Guided Inductive Synthesis Modulo Theories . in H Chockler & G Weissenbacher (eds), Computer Aided Verification (CAV 2018) Part I . Lecture Notes in Computer Science, vol. 10981, Cham, pp. 270-288, 30th International Conference on Computer Aided Verification, Oxford, United Kingdom, 14/07/18 . https://doi.org/10.1007/978-3-319-96145-3_15
Computer Aided Verification ISBN: 9783319961446
CAV (1)
Abate, A, David, C, Kesseli, P, Kroening, D & Polgreen, E 2018, Counterexample Guided Inductive Synthesis Modulo Theories . in H Chockler & G Weissenbacher (eds), Computer Aided Verification (CAV 2018) Part I . Lecture Notes in Computer Science, vol. 10981, Cham, pp. 270-288, 30th International Conference on Computer Aided Verification, Oxford, United Kingdom, 14/07/18 . https://doi.org/10.1007/978-3-319-96145-3_15
Computer Aided Verification ISBN: 9783319961446
CAV (1)
Program synthesis is the mechanized construction of software. One of the main difficulties is the efficient exploration of the very large solution space, and tools often require a user-provided syntactic restriction of the search space. We propose a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7c9918232de80f02483d1c4acff5811f
https://research-information.bris.ac.uk/ws/files/225506334/978_3_319_96145_3_283_301.pdf
https://research-information.bris.ac.uk/ws/files/225506334/978_3_319_96145_3_283_301.pdf
Publikováno v:
David, C, Kesseli, P, Kroening, D & Lewis, M 2018, ' Program Synthesis for Program Analysis ', ACM Transactions of Programming Languages and Systems, vol. 40, no. 2, 5, pp. 1-45 . https://doi.org/10.1145/3174802
In this article, we propose a unified framework for designing static analysers based on program synthesis . For this purpose, we identify a fragment of second-order logic with restricted quantification that is expressive enough to model numerous stat
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7fcc632e95a4605e3246fee6ad522185
Publikováno v:
Computer Aided Verification ISBN: 9783319961446
CAV (1)
CAV (1)
We present a bounded model checking tool for verifying Java bytecode, which is built on top of the CPROVER framework, named Java Bounded Model Checker (JBMC). JBMC processes Java bytecode together with a model of the standard Java libraries and check
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::8dad2a00ad68e96fb95d3e2ad4d4fce8
https://doi.org/10.1007/978-3-319-96145-3_10
https://doi.org/10.1007/978-3-319-96145-3_10
Autor:
Cristina David, Pascal Kesseli, Lucas C. Cordeiro, Iury Bessa, Dario Cattaruzza, Daniel Kroening, Alessandro Abate
Publikováno v:
Abate, A, Bessa, L, Cattaruzza, D, Cordeiro, L, David, C, Kesseli, P & Kroening, D 2017, Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants . in HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems : Computation and Control . Association for Computing Machinery (ACM), pp. 197–206, ACM International Conference on Hybrid Systems, Pittsburgh, Pennsylvania, United States, 18/04/17 . https://doi.org/10.1145/3049797.3049802
Abate, A, Bessa, I, Cattaruzza, D, Cordeiro, L, David, C, Kesseli, P & Kroening, D 2017, ' Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants ', HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, pp. 197-206 . https://doi.org/10.1145/3049797.3049802
Abate, A, Bessa, I, Cattaruzza, D, Cordeiro, L, David, C, Kesseli, P & Kroening, D 2017, ' Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants ', HSCC '17: Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control, pp. 197-206 . https://doi.org/10.1145/3049797.3049802
Modern control is implemented with digital microcontrollers, embedded within a dynamical plant that represents physical components. We present a new algorithm based on counter-example guided inductive synthesis that automates the design of digital co
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2bef3de02beb09aa6ecb59a7138896c5
https://ora.ox.ac.uk/objects/uuid:9362b4bf-6535-4db0-92fa-3d634ea6e651
https://ora.ox.ac.uk/objects/uuid:9362b4bf-6535-4db0-92fa-3d634ea6e651
Autor:
Peter Schrammel, Daniel Kroening, Philippa Conmy, Adam Nellis, Michael Tautschnig, Pascal Kesseli
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319406473
NFM
NFM
The malfunction of safety-critical systems may cause damage to people and the environment. Software within those systems is rigorously designed and verified according to domain specific guidance, such as ISO26262 for automotive safety. This paper des
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4836850563af462c9b9e4eee983c574e
http://sro.sussex.ac.uk/id/eprint/61596/1/nfm16.pdf
http://sro.sussex.ac.uk/id/eprint/61596/1/nfm16.pdf