-
Patch Space Exploration using Static Analysis Feedback
Authors:
Yuntong Zhang,
Andreea Costea,
Ridwan Shariffdeen,
Davin McCall,
Abhik Roychoudhury
Abstract:
Automated Program Repair (APR) techniques typically rely on a given test-suite to guide the repair process. Apart from the need to provide test oracles, this makes the produced patches prone to test data over-fitting. In this work, instead of relying on test cases, we show how to automatically repair memory safety issues, by leveraging static analysis (specifically Incorrectness Separation Logic)…
▽ More
Automated Program Repair (APR) techniques typically rely on a given test-suite to guide the repair process. Apart from the need to provide test oracles, this makes the produced patches prone to test data over-fitting. In this work, instead of relying on test cases, we show how to automatically repair memory safety issues, by leveraging static analysis (specifically Incorrectness Separation Logic) to guide repair. Our proposed approach learns what a desirable patch is by inspecting how close a patch is to fixing the bug based on the feedback from incorrectness separation logic based static analysis (specifically the Pulse analyser), and turning this information into a distribution of probabilities over context free grammars. Furthermore, instead of focusing on heuristics for reducing the search space of patches, we make repair scalable by creating classes of equivalent patches according to the effect they have on the symbolic heap, and then invoking the validation oracle only once per class of patch equivalence. This allows us to efficiently discover repairs even in the presence of a large pool of patch candidates offered by our generic patch synthesis mechanism. Experimental evaluation of our approach was conducted by repairing real world memory errors in OpenSSL, swoole and other subjects. The evaluation results show the scalability and efficacy of our approach in automatically producing high quality patches.
△ Less
Submitted 1 August, 2023;
originally announced August 2023.
-
Automated Modular Verification for Race-Free Channels with Implicit and Explicit Synchronization
Authors:
Andreea Costea,
Wei-Ngan Chin,
Florin Craciun,
Shengchao Qin
Abstract:
Ensuring the correctness of software for communication centric programs is important but challenging. Previous approaches, based on session types, have been intensively investigated over the past decade. They provide a concise way to express protocol specifications and a lightweight approach for checking their implementation. Current solutions are based on only implicit synchronization, and are ba…
▽ More
Ensuring the correctness of software for communication centric programs is important but challenging. Previous approaches, based on session types, have been intensively investigated over the past decade. They provide a concise way to express protocol specifications and a lightweight approach for checking their implementation. Current solutions are based on only implicit synchronization, and are based on the less precise types rather than logical formulae. In this paper, we propose a more expressive session logic to capture multiparty protocols. By using two kinds of ordering constraints, namely "happens-before" <HB and "communicates-before" <CB, we show how to ensure from first principle race-freedom over common channels. Our approach refines each specification with both assumptions and proof obligations to ensure compliance to some global protocol. Each specification is then projected for each party and then each channel, to allow cooperative proving through localized automated verification. Our primary goal in automated verification is to ensure race-freedom and communication-safety, but the approach is extensible for deadlock-freedom as well. We shall also describe how modular protocols can be captured and handled by our approach.
△ Less
Submitted 24 September, 2021;
originally announced September 2021.
-
HIPPODROME: Data Race Repair using Static Analysis Summaries
Authors:
Andreea Costea,
Abhishek Tiwari,
Sigmund Chianasta,
Kishore R,
Abhik Roychoudhury,
Ilya Sergey
Abstract:
Implementing bug-free concurrent programs is a challenging task in modern software development. State-of-the-art static analyses find hundreds of concurrency bugs in production code, scaling to large codebases. Yet, fixing these bugs in constantly changing codebases represents a daunting effort for programmers, particularly because a fix in the concurrent code can introduce other bugs in a subtle…
▽ More
Implementing bug-free concurrent programs is a challenging task in modern software development. State-of-the-art static analyses find hundreds of concurrency bugs in production code, scaling to large codebases. Yet, fixing these bugs in constantly changing codebases represents a daunting effort for programmers, particularly because a fix in the concurrent code can introduce other bugs in a subtle way.
In this work, we show how to harness compositional static analysis for concurrency bug detection, to enable a new Automated Program Repair (APR) technique for data races in large concurrent Java codebases. The key innovation of our work is an algorithm that translates procedure summaries inferred by the analysis tool for the purpose of bug reporting, into small local patches that fix concurrency bugs (without introducing new ones). This synergy makes it possible to extend the virtues of compositional static concurrency analysis to APR, making our approach effective (it can detect and fix many more bugs than existing tools for data race repair), scalable (it takes seconds to analyse and suggest fixes for sizeable codebases), and usable (generally, it does not require annotations from the users and can perform continuous automated repair). Our study conducted on popular open-source projects has confirmed that our tool automatically produces concurrency fixes similar to those proposed by the developers in the past.
△ Less
Submitted 6 August, 2021; v1 submitted 5 August, 2021;
originally announced August 2021.
-
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -- Extended Version
Authors:
Andreea Costea,
Amy Zhu,
Nadia Polikarpova,
Ilya Sergey
Abstract:
In program synthesis there is a well-known trade-off between concise and strong specifications: if a specification is too verbose, it might be harder to write than the program; if it is too weak, the synthesised program might not match the user's intent. In this work we explore the use of annotations for restricting memory access permissions in program synthesis, and show that they can make specif…
▽ More
In program synthesis there is a well-known trade-off between concise and strong specifications: if a specification is too verbose, it might be harder to write than the program; if it is too weak, the synthesised program might not match the user's intent. In this work we explore the use of annotations for restricting memory access permissions in program synthesis, and show that they can make specifications much stronger while remaining surprisingly concise. Specifically, we enhance Synthetic Separation Logic (SSL), a framework for synthesis of heap-manipulating programs, with the logical mechanism of read-only borrows. We observe that this minimalistic and conservative SSL extension benefits the synthesis in several ways, making it more (a) expressive (stronger correctness guarantees are achieved with a modest annotation overhead), (b) effective (it produces more concise and easier-to-read programs), (c) efficient (faster synthesis), and (d) robust (synthesis efficiency is less affected by the choice of the search heuristic). We explain the intuition and provide formal treatment for read-only borrows. We substantiate the claims (a)--(d) by describing our quantitative evaluation of the borrowing-aware synthesis implementation on a series of standard benchmark specifications for various heap-manipulating programs.
△ Less
Submitted 29 January, 2020;
originally announced January 2020.
-
Algorithms of evaluation of the waiting time and the modelling of the terminal activity
Authors:
Gh. Miscoi,
A. Costea,
R. I. Ţicu,
C. Pomazan
Abstract:
This paper approaches the application of the waiting model with Poisson inputs and priorities in the port activity. The arrival of ships in the maritime terminal is numerically modelled, and specific parameters for the distribution functions of service and of inputs are determined, in order to establish the waiting time of ships in the seaport and a stationary process. The modelling is based on wa…
▽ More
This paper approaches the application of the waiting model with Poisson inputs and priorities in the port activity. The arrival of ships in the maritime terminal is numerically modelled, and specific parameters for the distribution functions of service and of inputs are determined, in order to establish the waiting time of ships in the seaport and a stationary process. The modelling is based on waiting times and on the traffic coefficient.
△ Less
Submitted 20 March, 2019;
originally announced March 2019.
-
A modelling system for seaport activities
Authors:
Alina Costea,
Ionela Rodica Ticu,
Gheorghe Mishkoy
Abstract:
In this paper we shall approach a modelling system for seaport activities based on the average waiting time and average queue length of ships in the seaport. We shall propose some suggestions for deepening and expanding this modelling system.
In this paper we shall approach a modelling system for seaport activities based on the average waiting time and average queue length of ships in the seaport. We shall propose some suggestions for deepening and expanding this modelling system.
△ Less
Submitted 19 March, 2019;
originally announced March 2019.
-
Numerical simulations of the nonlinear Molodensky problem
Authors:
Lothar Banz,
Adrian Costea,
Heiko Gimperlein,
Ernst P. Stephan
Abstract:
We present a boundary element method to compute numerical approximations to the non-linear Molodensky problem, which reconstructs the surface of the earth from the gravitational potential and the gravity vector. Our solution procedure solves a sequence of exterior oblique Robin problems and is based on a Nash-Hörmander iteration. We apply smoothing with the heat equation to overcome a loss of deri…
▽ More
We present a boundary element method to compute numerical approximations to the non-linear Molodensky problem, which reconstructs the surface of the earth from the gravitational potential and the gravity vector. Our solution procedure solves a sequence of exterior oblique Robin problems and is based on a Nash-Hörmander iteration. We apply smoothing with the heat equation to overcome a loss of derivatives in the surface update. Numerical results compare the error between the approximation and the exact solution in a model problem.
△ Less
Submitted 12 August, 2013;
originally announced August 2013.
-
A Nash-Hormander iteration and boundary elements for the Molodensky problem
Authors:
Adrian Costea,
Heiko Gimperlein,
Ernst P. Stephan
Abstract:
We investigate the numerical approximation of the nonlinear Molodensky problem, which reconstructs the surface of the earth from the gravitational potential and the gravity vector. The method, based on a smoothed Nash-Hormander iteration, solves a sequence of exterior oblique Robin problems and uses a regularization based on a higher-order heat equation to overcome the loss of derivatives in the s…
▽ More
We investigate the numerical approximation of the nonlinear Molodensky problem, which reconstructs the surface of the earth from the gravitational potential and the gravity vector. The method, based on a smoothed Nash-Hormander iteration, solves a sequence of exterior oblique Robin problems and uses a regularization based on a higher-order heat equation to overcome the loss of derivatives in the surface update. In particular, we obtain a quantitative a priori estimate for the error after m steps, justify the use of smoothing operators based on the heat equation, and comment on the accurate evaluation of the Hessian of the gravitational potential on the surface, using a representation in terms of a hypersingular integral. A boundary element method is used to solve the exterior problem. Numerical results compare the error between the approximation and the exact solution in a model problem.
△ Less
Submitted 12 August, 2013;
originally announced August 2013.
-
High precision modeling at the 10^{-20} level
Authors:
M. Andres,
L. Banz,
A. Costea,
E. Hackmann,
S. Herrmann,
C. Lämmerzahl,
L. Nesemann,
B. Rievers,
E. P. Stephan
Abstract:
The requirements for accurate numerical simulation are increasing constantly. Modern high precision physics experiments now exceed the achievable numerical accuracy of standard commercial and scientific simulation tools. One example are optical resonators for which changes in the optical length are now commonly measured to 10^{-15} precision. The achievable measurement accuracy for resonators and…
▽ More
The requirements for accurate numerical simulation are increasing constantly. Modern high precision physics experiments now exceed the achievable numerical accuracy of standard commercial and scientific simulation tools. One example are optical resonators for which changes in the optical length are now commonly measured to 10^{-15} precision. The achievable measurement accuracy for resonators and cavities is directly influenced by changes in the distances between the optical components. If deformations in the range of 10^{-15} occur, those effects cannot be modeled and analysed any more with standard methods based on double precision data types. New experimental approaches point out that the achievable experimental accuracies may improve down to the level of 10^{-17} in the near future. For the development and improvement of high precision resonators and the analysis of experimental data, new methods have to be developed which enable the needed level of simulation accuracy. Therefore we plan the development of new high precision algorithms for the simulation and modeling of thermo-mechanical effects with an achievable accuracy of 10^{-20}. In this paper we analyse a test case and identify the problems on the way to this goal.
△ Less
Submitted 5 January, 2011;
originally announced January 2011.
