Literatura científica selecionada sobre o tema "Why3 tool for deductive verification"
Crie uma referência precisa em APA, MLA, Chicago, Harvard, e outros estilos
Consulte a lista de atuais artigos, livros, teses, anais de congressos e outras fontes científicas relevantes para o tema "Why3 tool for deductive verification".
Ao lado de cada fonte na lista de referências, há um botão "Adicionar à bibliografia". Clique e geraremos automaticamente a citação bibliográfica do trabalho escolhido no estilo de citação de que você precisa: APA, MLA, Harvard, Chicago, Vancouver, etc.
Você também pode baixar o texto completo da publicação científica em formato .pdf e ler o resumo do trabalho online se estiver presente nos metadados.
Artigos de revistas sobre o assunto "Why3 tool for deductive verification"
Shelekhov, Vladimir Ivanovich. "TRANSFORMATION AND VERIFICATION OF THE OS PROGRAM SORTING DEVICES IN A COMPUTER BUS". System Informatics, n.º 18 (2021): 1–34. http://dx.doi.org/10.31144/si.2307-6410.2021.n18.p1-34.
Texto completo da fonteFortin, Jean, e Frédéric Gava. "BSP-Why: A Tool for Deductive Verification of BSP Algorithms with Subgroup Synchronisation". International Journal of Parallel Programming 44, n.º 3 (31 de março de 2015): 574–97. http://dx.doi.org/10.1007/s10766-015-0360-y.
Texto completo da fonteSantos, César, Francisco Martins e Vasco Thudichum Vasconcelos. "Deductive Verification of Parallel Programs Using Why3". Electronic Proceedings in Theoretical Computer Science 189 (19 de agosto de 2015): 128–42. http://dx.doi.org/10.4204/eptcs.189.11.
Texto completo da fonteShelekhov, V. I. "Applying Program Transformations for Deductive Verification of the List Reverse Program". Programmnaya Ingeneria 12, n.º 3 (19 de maio de 2021): 127–39. http://dx.doi.org/10.17587/prin.12.127-139.
Texto completo da fonteLanzinger, Florian, Alexander Weigl, Mattias Ulbrich e Werner Dietl. "Scalability and precision by combining expressive type systems and deductive verification". Proceedings of the ACM on Programming Languages 5, OOPSLA (20 de outubro de 2021): 1–29. http://dx.doi.org/10.1145/3485520.
Texto completo da fonteWatanabe, Yasunari, Kiran Gopinathan, George Pîrlea, Nadia Polikarpova e Ilya Sergey. "Certifying the synthesis of heap-manipulating programs". Proceedings of the ACM on Programming Languages 5, ICFP (22 de agosto de 2021): 1–29. http://dx.doi.org/10.1145/3473589.
Texto completo da fonteCohen, Joshua M., e Philip Johnson-Freyd. "A Formalization of Core Why3 in Coq". Proceedings of the ACM on Programming Languages 8, POPL (5 de janeiro de 2024): 1789–818. http://dx.doi.org/10.1145/3632902.
Texto completo da fonteDevyanin, P. N., e M. A. Leonova. "The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB". Prikladnaya Diskretnaya Matematika, n.º 52 (2021): 83–96. http://dx.doi.org/10.17223/20710410/52/5.
Texto completo da fonteElad, Neta, Oded Padon e Sharon Shoham. "An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification". Proceedings of the ACM on Programming Languages 8, POPL (5 de janeiro de 2024): 970–1000. http://dx.doi.org/10.1145/3632875.
Texto completo da fonteShelekhov, Vladimir Ivanovich. "COMPARISON OF AUTOMATA-BASED ENGINEERING METHOD AND EVENT-B MODELING METHOD". System informatics, n.º 18 (2021): 53–84. http://dx.doi.org/10.31144/si.2307-6410.2021.n18.p53-84.
Texto completo da fonteTeses / dissertações sobre o assunto "Why3 tool for deductive verification"
Parreira, Pereira Mário José. "Tools and Techniques for the Verification of Modular Stateful Code". Thesis, Université Paris-Saclay (ComUE), 2018. http://www.theses.fr/2018SACLS605/document.
Texto completo da fonteThis thesis is set in the field of formal methods, more precisely in the domain of deductive program verification. Our working context is the Why3 framework, a set of tools to implement, formally specify, and prove programs usingoff-the-shelf theorem provers. Why3 features a programming language,called WhyML, designed with verification in mind. An important feature of WhyML is ghost code: portions of the program that are introduced for the sole purpose of specification andverification. When it comes to get an executable implementation, ghost code is removed by an automatic process called extraction. One of the main contributions of this thesis is the formalization and implementation of Why3's extraction. The formalization consists in showing that the extracted program preserves the same operational behavior as the original source code, based on a type and effect system. The new extraction mechanism has been successfully used to get correct-by-construction OCaml modules, which are part of averified OCaml library of data structures and algorithms. This verification effort led to two other contributions of this thesis.The first is a systematic approach to the verification ofpointer-based data structures using ghost models of fragments of the heap. A fully automatic verification of a union-find data structure was achieved using this technique. The second contribution is a modular way to reason about iteration, independently of the underlying implementation. Several cursors and higher-orderiterators have been specified and verified with this approach
Herms, Paolo. "Certification of a Tool Chain for Deductive Program Verification". Phd thesis, Université Paris Sud - Paris XI, 2013. http://tel.archives-ouvertes.fr/tel-00789543.
Texto completo da fonteGondelman, Léon. "Un système de types pragmatique pour la vérification déductive des programmes". Thesis, Université Paris-Saclay (ComUE), 2016. http://www.theses.fr/2016SACLS583/document.
Texto completo da fonteThis thesis is conducted in the framework of deductive software verification.is aims to formalize some concepts that are implemented in the verification tool Why3. The main idea is to explore solutions that a type system based approach can bring to deductive verification. First, we focus our attention on the notion of ghost code, a technique that is used in most of modern verification tools and which consists in giving to some parts of specification the appearance of operational code. Using ghost code correctly requires various precautions since the ghost code must never interfere with the operational code. The first chapter presents a type system with effects illustrating how ghost code can be used in a way which is both correct and expressive. The second chapter addresses some questions related to verification of programs with pointers in the presence of aliasing, i.e. when several pointers handled by a program denote a same memory cell. Rather than moving towards to approaches that address the problem in all its complexity to the costs of abandoning the framework of Hoare logic, we present a type system with effects and singleton regions which resolves a liasing issues by performing a static control of aliases even before the proof obligations are generated. Although our system is limited to pointers whose identity must be known statically, we observe that it fits for most of the code we want to verify. Finally, we focus our attention on a situation where there exists an abstraction barrier between the user's code and the one of the libraries which it depends on. That means that libraries provide the user a set of functions and of data structures, without revealing details of their implementation. When programs are developed in a such modular way, verification must be modular it self. It means that the verification of user's code must take into account only function contracts supplied by libraries while the verification of libraries must ensure that their implementations refine correctly the exposed entities. The third chapter extends the system presented in the previous chapter with these concepts of modularity and data refinement
Rieu, Raphaël. "Development and verification of arbitrary-precision integer arithmetic libraries". Electronic Thesis or Diss., université Paris-Saclay, 2020. http://www.theses.fr/2020UPASG023.
Texto completo da fonteArbitrary-precision integer arithmetic algorithms are used in contexts where both their performance and their correctness are critical, such as cryptographic software or computer algebra systems. GMP is a very widely-used arbitrary-precision integer arithmetic library. It features state-of-the-art algorithms that are intricate enough that their formal verification is both justified and difficult. This thesis tackles the formal verification of the functional correctness of a large fragment of GMP using the Why3 deductive verification platform.In order to make this verification possible, I have made several additions to Why3 that enable the verification of C programs. Why3 features a functional programming and specification language called WhyML. I have developed models of the memory management and datatypes of the C language, allowing me to reimplement GMP's algorithms in WhyML and formally verify them. I have also extended Why3's extraction mechanism so that WhyML programs can be compiled to idiomatic C code, where only OCaml used to be supported.The compilation of my WhyML algorithms results in a verified C library called WhyMP. It implements many state-of-the-art algorithms from GMP, with almost all of the optimization tricks preserved. WhyMP is compatible with GMP and performance-competitive with the assembly-free version. It goes far beyond existing verified arbitrary-precision arithmetic libraries, and is arguably the most ambitious existing Why3 development in terms of size and proof effort.In an attempt to increase the degree of automation of my proofs, I have also added to Why3 a framework for proofs by reflection. It enables Why3 users to easily write dedicated decision procedures that are formally verified programs and make full use of WhyML's imperative features. Using this new framework, I was able to replace hundreds of handwritten proof annotations in my GMP verification by automated proofs
Capítulos de livros sobre o assunto "Why3 tool for deductive verification"
Pereira, Mário, e António Ravara. "Cameleer: A Deductive Verification Tool for OCaml". In Computer Aided Verification, 677–89. Cham: Springer International Publishing, 2021. http://dx.doi.org/10.1007/978-3-030-81688-9_31.
Texto completo da fonteBlazy, Sandrine. "Teaching Deductive Verification in Why3 to Undergraduate Students". In Formal Methods Teaching, 52–66. Cham: Springer International Publishing, 2019. http://dx.doi.org/10.1007/978-3-030-32441-4_4.
Texto completo da fonteBeckert, Bernhard, Richard Bubel, Reiner Hähnle e Mattias Ulbrich. "Towards a Usable and Sustainable Deductive Verification Tool". In Leveraging Applications of Formal Methods, Verification and Validation. Software Engineering, 281–300. Cham: Springer Nature Switzerland, 2022. http://dx.doi.org/10.1007/978-3-031-19756-7_16.
Texto completo da fonteBernier, Téo, Yani Ziani, Nikolai Kosmatov e Frédéric Loulergue. "Combining Deductive Verification with Shape Analysis". In Fundamental Approaches to Software Engineering, 280–89. Cham: Springer Nature Switzerland, 2024. http://dx.doi.org/10.1007/978-3-031-57259-3_14.
Texto completo da fonteManna, Zohar, Nikolaj S. Bjørner, Anca Browne, Michael Colón, Bernd Finkbeiner, Mark Pichora, Henny B. Sipma e Tomás E. Uribe. "An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems". In Tool Support for System Specification, Development and Verification, 174–88. Vienna: Springer Vienna, 1999. http://dx.doi.org/10.1007/978-3-7091-6355-9_13.
Texto completo da fonteNagasamudram, Ramana, Anindya Banerjee e David A. Naumann. "The WhyRel Prototype for Modular Relational Verification of Pointer Programs". In Tools and Algorithms for the Construction and Analysis of Systems, 133–51. Cham: Springer Nature Switzerland, 2023. http://dx.doi.org/10.1007/978-3-031-30820-8_11.
Texto completo da fonteMonti, Raúl E., Robert Rubbens e Marieke Huisman. "On Deductive Verification of an Industrial Concurrent Software Component with VerCors". In Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles, 517–34. Cham: Springer International Publishing, 2022. http://dx.doi.org/10.1007/978-3-031-19849-6_29.
Texto completo da fontevan Oorschot, Dré, Marieke Huisman e Ömer Şakar. "First Steps towards Deductive Verification of LLVM IR". In Fundamental Approaches to Software Engineering, 290–303. Cham: Springer Nature Switzerland, 2024. http://dx.doi.org/10.1007/978-3-031-57259-3_15.
Texto completo da fonteCorrenson, Loïc, Allan Blanchard, Adel Djoudi e Nikolai Kosmatov. "Automate where Automation Fails: Proof Strategies for Frama-C/WP". In Tools and Algorithms for the Construction and Analysis of Systems, 331–39. Cham: Springer Nature Switzerland, 2024. http://dx.doi.org/10.1007/978-3-031-57246-3_18.
Texto completo da fontevan den Haak, Lars B., Anton Wijs, Marieke Huisman e Mark van den Brand. "$${\textsc {HaliVer}}$$: Deductive Verification and Scheduling Languages Join Forces". In Tools and Algorithms for the Construction and Analysis of Systems, 71–89. Cham: Springer Nature Switzerland, 2024. http://dx.doi.org/10.1007/978-3-031-57256-2_4.
Texto completo da fonteTrabalhos de conferências sobre o assunto "Why3 tool for deductive verification"
Шелехов, В. И. "DEDUCTIVE VERIFICATION OF A SIMPLE MUTUAL EXCLUSION PROTOCOL". In Сборник трудов XVIII Российской конференции "РАСПРЕДЕЛЕННЫЕ ИНФОРМАЦИОННО-ВЫЧИСЛИТЕЛЬНЫЕ РЕСУРСЫ". Crossref, 2023. http://dx.doi.org/10.25743/dir.2022.88.64.040.
Texto completo da fonte