Zobrazeno 1 - 10
of 50
pro vyhledávání: '"PREVOSTO, VIRGILE"'
The use of function contracts to specify the behavior of functions often remains limited to the scope of a single function call. Relational properties link several function calls together within a single specification. They can express more advanced
Externí odkaz:
http://arxiv.org/abs/2202.10349
Publikováno v:
EPTCS 310, 2019
This volume contains the proceedings of F-IDE 2019, the fifth international workshop on Formal Integrated Development Environment, which was held on October 7, 2019 in Porto, Portugal, as part of FM'19, the 3rd World Congress on Formal Methods. High
Externí odkaz:
http://arxiv.org/abs/1912.09611
Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related properties of a whole s
Externí odkaz:
http://arxiv.org/abs/1811.10509
Publikováno v:
EPTCS 284, 2018
This volume contains the proceedings of F-IDE 2018, the fourth international workshop on Formal Integrated Development Environment, which was held as a FLoC 2018 satellite event, on July 14, 2018, in Oxford, England. High levels of safety, security a
Externí odkaz:
http://arxiv.org/abs/1811.09014
This paper investigates the connexion between the Kannan-Lipton Orbit Problem and the polynomial invariant generator algorithm PILA based on eigenvectors computation. Namely, we reduce the problem of generating linear and polynomial certificates of n
Externí odkaz:
http://arxiv.org/abs/1803.09511
Function contracts are a well-established way of formally specifying the intended behavior of a function. However, they usually only describe what should happen during a single call. Relational properties, on the other hand, link several function cal
Externí odkaz:
http://arxiv.org/abs/1801.06876
Autor:
Marcozzi, Michaël, Bardin, Sébastien, Kosmatov, Nikolai, Papadakis, Mike, Prevosto, Virgile, Correnson, Loïc
Testing is the primary approach for detecting software defects. A major challenge faced by testers lies in crafting efficient test suites, able to detect a maximum number of bugs with manageable effort. To do so, they rely on coverage criteria, which
Externí odkaz:
http://arxiv.org/abs/1708.08765
When proving invariance properties of a program, we face two problems. The first problem is related to the necessity of proving tautologies of considered assertion language, whereas the second manifests in the need of finding sufficiently strong inva
Externí odkaz:
http://arxiv.org/abs/1611.07753
Publikováno v:
Automated Technology for Verification and Analysis 2016 Volume 9938 of the series Lecture Notes in Computer Science pp 479-494
We present in this paper a new technique for generating polynomial invariants, divided in two independent parts : a procedure that reduces polynomial assignments composed loops analysis to linear loops under certain hypotheses and a procedure for gen
Externí odkaz:
http://arxiv.org/abs/1611.07726