Search

Your search keyword '"Loop invariant"' showing total 486 results
Start Over Descriptor "Loop invariant"
486 results on '"Loop invariant"'

1. Logic for reasoning about bugs in loops over data sequences (IFIL)

Author

Dmitry A. Kondratyev

Subjects
deductive verification, hoare logic, bug localization, program incorrectness, loop invariant, finite iteration, c-lightver, acl2, Information technology, T58.5-58.64
Abstract

Classic deductive verification is not focused on reasoning about program incorrectness. Reasoning about program incorrectness using formal methods is an important problem nowadays. Special logics such as Incorrectness Logic, Adversarial Logic, Local Completeness Logic, Exact Separation Logic and Outcome Logic have recently been proposed to address it. However, these logics have two disadvantages. One is that they are based on under-approximation approaches, while classic deductive verification is based on the over-approximation approach. One the other hand, the use of the classic approach requires defining loop invariants in a general case. The second disadvantage is that the use of generalized inference rules from these logics results in having to prove too complex formulas in simple cases. Our contribution is a new logic for solving these problems in the case of loops over data sequences. These loops are referred to as finite iterations. We call the proposed logic the Incorrectness Finite Iteration Logic (IFIL). We avoid defining invariants of finite iterations using a symbolic replacement of these loops with recursive functions. Our logic is based on special inference rules for finite iterations. These rules allow generating formulas with recursive functions corresponding to finite iterations. The validity of these formulas may indicate the presence of bugs in the finite iterations. This logic has been implemented in a new version of the C-lightVer system for deductive verification of C programs.

Published
2023
Full Text
View/download PDF

2. On How to Not Prove Faulty Controllers Safe in Differential Dynamic Logic

Author

Selvaraj, Yuvaraj, Krook, Jonas, Ahrendt, Wolfgang, Fabian, Martin, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Riesco, Adrian, editor, and Zhang, Min, editor

Published
2022
Full Text
View/download PDF

3. Nonlinear Program Construction and Verification Method Based on Partition Recursion and Morgan's Refinement Rules.

Author

WANG Changjing, CAO Zhongxiong, YU Chuling, WANG Changchang, HUANG Qing, and ZUO Zhengkang

Abstract

The traditional program refinement strategy cannot be refined to an executable program, and there are issues such as low verification reliability and automation. To solve the above problems, this paper proposes a nonlinear program construction and verification method based on partition recursion and Morgan's refinement rules. First, we use recursive definition technique to characterize the initial specification. The specification is then transformed into GCL(Guarded Command Language) programs using loop invariant derivation and Morgan's refinement rules. Furthermore, VCG (Verification Condition Generator) is used in the GCL program to generate the verification condition automatically. The Isabelle theorem prover then validates the GCL program's correctness. Finally, the GCL code generates a C++ executable program automatically via the conversion system. The effectiveness of this method is demonstrated using binary tree preorder traversal program construction and verification as an example. This method addresses the problem that the construction process's loop invariant is difficult to obtain and the refinement process is insufficiently detailed. At the same time, the method improves verification process automation and reduces the manual verification workload. [ABSTRACT FROM AUTHOR]

Published
2023
Full Text
View/download PDF

4. Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System.

Author

Kondratyev, D. A.

Abstract

The C-lightVer system for deductive verification of C programs has been developed at the Institute of Informatics Systems of the Siberian Branch of the Russian Academy of Sciences (IIS SB RAS). C-kernel is an intermediate verification language in this system. The cloud parallel programming system (CPPS) is also developed at the IIS SB RAS. Cloud Sisal is the input language of the CPPS system. The main feature of the CPPS system is the implicit parallel execution based on the automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is the automatic parallelization of such a superset of the C language that allows implementing automatic verification. Our solution is a superset of the C-kernel language such as the C-Sisal-kernel language. The first result presented in this article is an extension of C-kernel by Cloud-Sisal-kernel loops. As a consequence, the C-Sisal-kernel language is developed. The second result presented in this article is the extension of the C-kernel axiomatic semantics by an inference rule for Cloud-Sisal-kernel loops. This article also presents our approach to the problem of automating deductive verification in the case of definite iterations over data sequences. Such loops are called definite iterations. Our solution is a composition of a symbolic method of verification of definite iterations, verification condition metageneration, and mixed axiomatic semantics. The symbolic method of verification of definite iterations allows us to define inference rules for such loops without invariants. Symbolic replacement of definite iterations by recursive functions is the basis of this method. The resulting verification conditions using recursive functions correspond to the logical basis of the ACL2 prover. We use the ACL2 system based on computable recursive functions. Verification condition metageneration simplifies the implementation of new inference rules in the verification system. In some cases, the use of mixed axiomatic semantics leads to simpler verification conditions. [ABSTRACT FROM AUTHOR]

Published
2022
Full Text
View/download PDF

5. Full-program induction: verifying array programs sans loop invariants.

Author

Chakraborty, Supratik, Gupta, Ashutosh, and Unadkat, Divyesh

Subjects
*SOFTWARE verification, *ALGEBRAIC functions, *ELECTRONIC data processing, *PROGRAM transformation, *COMPUTER software
Abstract

Arrays are commonly used in a variety of software to store and process data in loops. Automatically proving safety properties of such programs that manipulate arrays is challenging. We present a novel verification technique, called full-program induction, for proving (a sub-class of) quantified as well as quantifier-free properties of programs manipulating arrays of parametric size N. Instead of inducting over individual loops, our technique inducts over the entire program (possibly containing multiple loops) directly via the program parameter N. The technique performs non-trivial transformations of the given program and pre-conditions during the inductive step. The transformations assist in effectively reducing the assertion checking problem by transforming a program with multiple loops to a program which has fewer and simpler loops or is loop free. Significantly, full-program induction does not require generation or use of loop-specific invariants. To assess the efficacy of our technique, we have developed a prototype tool called Vajra. We demonstrate the performance of Vajra vis-a-vis several state-of-the-art tools on a large set of array manipulating benchmarks from the international software verification competition (SV-COMP) and on several programs inspired by algebraic functions that perform polynomial computations. [ABSTRACT FROM AUTHOR]

Published
2022
Full Text
View/download PDF

6. Formal Development and Verification of Reusable Component in PAR Platform

Author

Hu, Qimin, Xue, Jinyun, You, Zhen, Cheng, Zhuo, Zuo, Zhengkang, Goos, Gerhard, Founding Editor, Hartmanis, Juris, Founding Editor, Bertino, Elisa, Editorial Board Member, Gao, Wen, Editorial Board Member, Steffen, Bernhard, Editorial Board Member, Woeginger, Gerhard, Editorial Board Member, Yung, Moti, Editorial Board Member, Miao, Huaikou, editor, Tian, Cong, editor, Liu, Shaoying, editor, and Duan, Zhenhua, editor

Published
2020
Full Text
View/download PDF

7. Towards Automatic Deductive Verification of C Programs with Sisal Loops Using the C-lightVer System

Author

Dmitry A. Kondratyev

Subjects
deductive verification, c-lightver, cloud parallel programming system, symbolic method of verification of definite iterations, loop invariant, acl2, Information technology, T58.5-58.64
Abstract

The C-lightVer system is developed in IIS SB RAS for C-program deductive verification. C-kernel is an intermediate verification language in this system. Cloud parallel programming system (CPPS) is also developed in IIS SB RAS. Cloud Sisal is an input language of CPPS. The main feature of CPPS is implicit parallel execution based on automatic parallelization of Cloud Sisal loops. Cloud-Sisal-kernel is an intermediate verification language in the CPPS system. Our goal is automatic parallelization of such a superset of C that allows implementing automatic verification. Our solution is such a superset of C-kernel as C-Sisal-kernel. The first result presented in this paper is an extension of C-kernel by Cloud-Sisal-kernel loops. We have obtained the C-Sisal-kernel language. The second result is an extension of C-kernel axiomatic semantics by inference rule for Cloud-Sisal-kernel loops. The paper also presents our approach to the problem of deductive verification automation in the case of finite iterations over data structures. This kind of loops is referred to as definite iterations. Our solution is a composition of symbolic method of verification of definite iterations, verification condition metageneration and mixed axiomatic semantics method. Symbolic method of verification of definite iterations allows defining inference rules for these loops without invariants. Symbolic replacement of definite iterations by recursive functions is the base of this method. Obtained verification conditions with applications of recursive functions correspond to logical base of ACL2 prover. We use ACL2 system based on computable recursive functions. Verification condition metageneration allows simplifying implementation of new inference rules in a verification system. The use of mixed axiomatic semantics results to simpler verification conditions in some cases.

Published
2021
Full Text
View/download PDF

8. Formal Specification and Verification for Real-Time Scheduling Based on PAR

Author

You, Zhen, Cheng, Zhuo, Xue, Jinyun, Hu, Qimin, Xie, Wuping, Hutchison, David, Series Editor, Kanade, Takeo, Series Editor, Kittler, Josef, Series Editor, Kleinberg, Jon M., Series Editor, Mattern, Friedemann, Series Editor, Mitchell, John C., Series Editor, Naor, Moni, Series Editor, Pandu Rangan, C., Series Editor, Steffen, Bernhard, Series Editor, Terzopoulos, Demetri, Series Editor, Tygar, Doug, Series Editor, Duan, Zhenhua, editor, Liu, Shaoying, editor, Tian, Cong, editor, and Nagoya, Fumiko, editor

Published
2019
Full Text
View/download PDF

9. Translation Validation of Loop Invariant Code Optimizations Involving False Computations

Author

Chouksey, Ramanuj, Karfa, Chandan, Bhaduri, Purandar, Barbosa, Simone Diniz Junqueira, Series editor, Chen, Phoebe, Series editor, Filipe, Joaquim, Series editor, Kotenko, Igor, Series editor, Sivalingam, Krishna M., Series editor, Washio, Takashi, Series editor, Yuan, Junsong, Series editor, Zhou, Lizhu, Series editor, Kaushik, Brajesh Kumar, editor, Dasgupta, Sudeb, editor, and Singh, Virendra, editor

Published
2017
Full Text
View/download PDF

10. Formal Development of Linear Structure Reusable Components in PAR Platform

Author

Hu, Qimin, Xue, Jinyun, You, Zhen, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Liu, Shaoying, editor, Duan, Zhenhua, editor, Tian, Cong, editor, and Nagoya, Fumiko, editor

Published
2017
Full Text
View/download PDF

11. Hierarchical Analysis of Loops With Relaxed Abstract Transformers.

Author

Yin, Banghu, Chen, Liqian, Liu, Jiangchao, and Wang, Ji

Subjects
*INFORMATION storage & retrieval systems, *CYBER physical systems, *ARTIFICIAL neural networks, *TRANSFER functions, *BIG data
Abstract

Numerical computation is often involved in software of embedded control systems, cyber-physical systems, artificial neural network systems, big data processing systems, etc. Automatically discovering numerical loop invariants is fundamental for checking the safety of such software. Abstract interpretation provides a framework to automatically discover sound invariants but which may be not precise enough due to over-approximations. One major source of precision loss is due to the limited linear expressiveness of most widely used numerical abstract domains and the widening operation. This becomes more serious when analyzing all variables simultaneously as a whole for programs that involve nonlinear behaviors. Based on the observation that the dependency among variables in a loop can be hierarchical, in this article, we propose a hierarchical static analysis to analyze a loop by utilizing relaxed abstract transformers. The main idea is to first partition all variables involved in a loop into different hierarchical layers, then compute invariants over the variables layer by layer in a bottom-up manner. During the iterative process, the computed invariants over lower layer variables are then used to relax transfer functions when analyzing the higher layer variables. One benefit of our method lies in that it can generate linear invariants to soundly enclose nonlinear behaviors in a loop. Finally, we present encouraging experimental results on benchmark programs involving nonlinear behaviors. [ABSTRACT FROM AUTHOR]

Published
2020
Full Text
View/download PDF

12. Counterexamples from Proof Failures in SPARK

Author

Hauzar, David, Marché, Claude, Moy, Yannick, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, De Nicola, Rocco, editor, and Kühn, Eva, editor

Published
2016
Full Text
View/download PDF

13. Research on Formal Development of Non-recursive Algorithms of Graph Search

Author

Hu, Qimin, Xue, Jinyun, You, Zhen, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Liu, Shaoying, editor, and Duan, Zhenhua, editor

Published
2016
Full Text
View/download PDF

14. Formal Specification with the Java Modeling Language

Author

Huisman, Marieke, Ahrendt, Wolfgang, Grahl, Daniel, Hentschel, Martin, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Ahrendt, Wolfgang, editor, Beckert, Bernhard, editor, Bubel, Richard, editor, Hähnle, Reiner, editor, Schmitt, Peter H., editor, and Ulbrich, Mattias, editor

Published
2016
Full Text
View/download PDF

15. A Fully Verified Container Library

Author

Polikarpova, Nadia, Tschannen, Julian, Furia, Carlo A., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Bjørner, Nikolaj, editor, and de Boer, Frank, editor

Published
2015
Full Text
View/download PDF

16. DynaMate: Dynamically Inferring Loop Invariants for Automatic Full Functional Verification

Author

Galeotti, Juan Pablo, Furia, Carlo A., May, Eva, Fraser, Gordon, Zeller, Andreas, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, and Yahav, Eran, editor

Published
2014
Full Text
View/download PDF

17. A Verification Condition Visualizer

Author

Jami, Madiha, Ireland, Andrew, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Giannakopoulou, Dimitra, editor, and Kroening, Daniel, editor

Published
2014
Full Text
View/download PDF

18. A Bounded Model Checker for SPARK Programs

Author

Lourenço, Cláudio Belo, Frade, Maria João, Pinto, Jorge Sousa, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Cassez, Franck, editor, and Raskin, Jean-François, editor

Published
2014
Full Text
View/download PDF

19. Tool Support for Teaching Hoare Logic

Author

Sznuk, Tadeusz, Schubert, Aleksy, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Giannakopoulou, Dimitra, editor, and Salaün, Gwen, editor

Published
2014
Full Text
View/download PDF

20. QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers

Author

Cox, Arlen, Chang, Bor-Yuh Evan, Sankaranarayanan, Sriram, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Kobsa, Alfred, editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Weikum, Gerhard, editor, Biere, Armin, editor, and Bloem, Roderick, editor

Published
2014
Full Text
View/download PDF

22. MinFinder: A New Approach in Sorting Algorithm.

Author

Rana, Md. Shohel, Hossin, Md Altab, Mahmud, S M Hasan, Jahan, Hosney, Satter, A.K.M. Zaidi, and Bhuiyan, Touhid

Subjects
EXTREME value theory, COMPUTER programming, ALGORITHMS, COMPUTER software, SPACETIME
Abstract

Sorting a set of unsorted items is a task that happens in computer programming while a computer program has to follow a sequence of precise directions to accomplish that task. In order to find things quickly by making extreme values easy to see, sorting algorithm refers to specifying a technique to arrange the data in a particular order or format where maximum of communal orders is in arithmetic or lexicographical order. A lot of sorting algorithms has already been developed and these algorithms have enhanced the performance in the factors including time and space complexity, stability, correctness, definiteness, finiteness, effectiveness, etc. A new approach has been proposed in this paper in sorting algorithm called MinFinder to overcome some of the downsides and performs better compared to some conventional algorithms in terms of stability, computational time, complexity analysis. [ABSTRACT FROM AUTHOR]

Published
2019
Full Text
View/download PDF

24. Verifying a Plaftorm for Digital Imaging: A Multi-tool Strategy

Author

Heras, Jónathan, Mata, Gadea, Romero, Ana, Rubio, Julio, Sáenz, Rubén, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Goebel, Randy, editor, Siekmann, Jörg, editor, Wahlster, Wolfgang, editor, Carette, Jacques, editor, Aspinall, David, editor, Lange, Christoph, editor, Sojka, Petr, editor, and Windsteiger, Wolfgang, editor

Published
2013
Full Text
View/download PDF

25. Whiley: A Platform for Research in Software Verification

Author

Pearce, David J., Groves, Lindsay, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Erwig, Martin, editor, Paige, Richard F., editor, and Van Wyk, Eric, editor

Published
2013
Full Text
View/download PDF

27. Using Dafny, an Automatic Program Verifier

Author

Herbert, Luke, Leino, K. Rustan M., Quaresma, Jose, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Meyer, Bertrand, editor, and Nordio, Martin, editor

Published
2012
Full Text
View/download PDF

28. Combining Analyses for C Program Verification

Author

Correnson, Loïc, Signoles, Julien, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Stoelinga, Mariëlle, editor, and Pinger, Ralf, editor

Published
2012
Full Text
View/download PDF

29. The COST IC0701 Verification Competition 2011

Author

Bormer, Thorsten, Brockschmidt, Marc, Distefano, Dino, Ernst, Gidon, Filliâtre, Jean-Christophe, Grigore, Radu, Huisman, Marieke, Klebanov, Vladimir, Marché, Claude, Monahan, Rosemary, Mostowski, Wojciech, Polikarpova, Nadia, Scheben, Christoph, Schellhorn, Gerhard, Tofan, Bogdan, Tschannen, Julian, Ulbrich, Mattias, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Beckert, Bernhard, editor, Damiani, Ferruccio, editor, and Gurov, Dilian, editor

Published
2012
Full Text
View/download PDF

30. Unbounded Symbolic Execution for Program Verification

Author

Jaffar, Joxan, Navas, Jorge A., Santosa, Andrew E., Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Khurshid, Sarfraz, editor, and Sen, Koushik, editor

Published
2012
Full Text
View/download PDF

31. Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data

Author

Bouajjani, Ahmed, Drăgoi, Cezara, Enea, Constantin, Sighireanu, Mihaela, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Kuncak, Viktor, editor, and Rybalchenko, Andrey, editor

Published
2012
Full Text
View/download PDF

32. Automatically Verifying Typing Constraints for a Data Processing Language

Author

Backes, Michael, Hriţcu, Cătălin, Tarrach, Thorsten, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Jouannaud, Jean-Pierre, editor, and Shao, Zhong, editor

Published
2011
Full Text
View/download PDF

33. Hardware-Dependent Proofs of Numerical Programs

Author

Nguyen, Thi Minh Tuyen, Marché, Claude, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Jouannaud, Jean-Pierre, editor, and Shao, Zhong, editor

Published
2011
Full Text
View/download PDF

34. Mutation in Linked Data Structures

Author

Maclean, Ewen, Ireland, Andrew, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Qin, Shengchao, editor, and Qiu, Zongyan, editor

Published
2011
Full Text
View/download PDF

35. FixBag: A Fixpoint Calculator for Quantified Bag Constraints

Author

Pham, Tuan-Hung, Trinh, Minh-Thai, Truong, Anh-Hoang, Chin, Wei-Ngan, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Gopalakrishnan, Ganesh, editor, and Qadeer, Shaz, editor

Published
2011
Full Text
View/download PDF

36. An Iterative Method for Generating Loop Invariants

Author

Chen, Shikun, Li, Zhoujun, Song, Xiaoyu, Li, Mengjun, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Atallah, Mikhail, editor, Li, Xiang-Yang, editor, and Zhu, Binhai, editor

Published
2011
Full Text
View/download PDF

37. Contract-Based Slicing

Author

da Cruz, Daniela, Henriques, Pedro Rangel, Sousa Pinto, Jorge, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Margaria, Tiziana, editor

Published
2010
Full Text
View/download PDF

38. A Shape Analysis for Non-linear Data Structures

Author

Cherini, Renato, Rearte, Lucas, Blanco, Javier, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Cousot, Radhia, editor, and Martel, Matthieu, editor

Published
2010
Full Text
View/download PDF

39. Towards Scalable Modular Checking of User-Defined Properties

Author

Ball, Thomas, Hackett, Brian, Lahiri, Shuvendu K., Qadeer, Shaz, Vanegue, Julien, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Leavens, Gary T., editor, O’Hearn, Peter, editor, and Rajamani, Sriram K., editor

Published
2010
Full Text
View/download PDF

41. Tracking Heaps That Hop with Heap-Hop

Author

Villard, Jules, Lozes, Étienne, Calcagno, Cristiano, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Esparza, Javier, editor, and Majumdar, Rupak, editor

Published
2010
Full Text
View/download PDF

42. PAR 平台中若干软件构件形式化验证技术研究.

Author

韻磨敵, 薛锦云, 屬 珍, and 程着

Abstract

PAR platform is a software platform developed by our research team to support software formality and automated development. The platform fully embodies the advantages of functional abstraction and data abstraction, thus making software development convenient and reliable. The key to achieving this performance is a batch of reusable software components. In order to ensure the correctness and reliability of the whole software platform, it is very important to ensure the correctness and reliability of the software components. In this paper, we select some typical software components in the PAR platform, formalize the semantics of the components in a formal way，and prove the correctness of the components with the help of the Coq theorem prover，hence improving the efficiency of software compoents' formal verification. [ABSTRACT FROM AUTHOR]

Published
2018
Full Text
View/download PDF

43. Verifying Component-Based Software: Deep Mathematics or Simple Bookkeeping?

Author

Kirschenbaum, Jason, Adcock, Bruce, Bronish, Derek, Smith, Hampton, Harton, Heather, Sitaraman, Murali, Weide, Bruce W., Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Edwards, Stephen H., editor, and Kulczycki, Gregory, editor

Published
2009
Full Text
View/download PDF

44. Hagenberg Research: Introduction

Author

Buchberger, Bruno, Buchberger, Bruno, editor, Affenzeller, Michael, editor, Ferscha, Alois, editor, Haller, Michael, editor, Jebelean, Tudor, editor, Klement, Erich Peter, editor, Paule, Peter, editor, Pomberger, Gustav, editor, Schreiner, Wolfgang, editor, Stubenrauch, Robert, editor, Wagner, Roland, editor, Weiß, Gerhard, editor, and Windsteiger, Wolfgang, editor

Published
2009
Full Text
View/download PDF

45. Towards the Integration of Symbolic and Numerical Static Analysis

Author

Venet, Arnaud, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Meyer, Bertrand, editor, and Woodcock, Jim, editor

Published
2008
Full Text
View/download PDF

46. Specification and Checking of Software Contracts for Conditional Information Flow

Author

Amtoft, Torben, Hatcliff, John, Rodríguez, Edwin, Robby, Hoag, Jonathan, Greve, David, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Cuellar, Jorge, editor, Maibaum, Tom, editor, and Sere, Kaisa, editor

Published
2008
Full Text
View/download PDF

47. Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving

Author

Maus, Stefan, Moskal, Michał, Schulte, Wolfram, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Meseguer, José, editor, and Roşu, Grigore, editor

Published
2008
Full Text
View/download PDF

48. Explaining Verification Conditions

Author

Denney, Ewen, Fischer, Bernd, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Meseguer, José, editor, and Roşu, Grigore, editor

Published
2008
Full Text
View/download PDF

49. Automatic Derivation of Linear Algebra Algorithms with Application to Control Theory

Author

Bientinesi, Paolo, Kolos, Sergey, van de Geijn, Robert A., Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Dongarra, Jack, editor, Madsen, Kaj, editor, and Waśniewski, Jerzy, editor

Published
2006
Full Text
View/download PDF

50. A Logic of Reachable Patterns in Linked Data-Structures

Author

Yorsh, Greta, Rabinovich, Alexander, Sagiv, Mooly, Meyer, Antoine, Bouajjani, Ahmed, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Dough, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Aceto, Luca, editor, and Ingólfsdóttir, Anna, editor

Published
2006
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results