An official website of the United States government
Modular verification tools allow programmers to compositionally specify and prove function specifications. When using a modular verifier, proving a specification about a functionfrequires additional specifications for the functions called byf. With existing state of the art tools, programmers must manually write the specifications for callee functions. We present a counterexample guided algorithm to automatically infer these specifications. The algorithm is parameterized over a verifier, counterexample generator, and constraint guided synthesizer. We show that if each of these three components is sound and complete over a finite set of possible specifications, our algorithm is sound and complete as well. Additionally, we introducesize-boundedsynthesis functions, which extends our completeness result to an infinite set of possible specifications. In particular, we describe a size-bounded synthesis function for linear integer arithmetic constraints. We conclude with an evaluation demonstrating our technique on a variety of benchmarks. When using a modular verifier, proving a specification about a functionfrequires additional specifications for the functions called byf. With existing state of the art tools, programmers must manually write the specifications for callee functions. We present a counterexample guided algorithm to automatically infer these specifications. The algorithm is parameterized over a verifier, counterexample generator, and constraint guided synthesizer. We show that if each of these three components is sound and complete over a finite set of possible specifications, our algorithm is sound and complete as well. Additionally, we introducesize-boundedsynthesis functions, which extends our completeness result to an infinite set of possible specifications. In particular, we describe a size-bounded synthesis function for linear integer arithmetic constraints. We conclude with an evaluation demonstrating our technique on a variety of benchmarks.
more »
« less
Accelerating Protocol Synthesis and Detecting Unrealizability with Interpretation Reduction
Abstract We present a novel counterexample-guided, sketch-based method for the synthesis of symbolic distributed protocols in TLA+. Our method’s chief novelty lies in a new search space reduction technique called interpretation reduction, which allows to not only eliminate incorrect candidate protocols before they are sent to the verifier, but also to avoid enumerating redundant candidates in the first place. Further performance improvements are achieved by an advanced technique for exact generalization of counterexamples. Experiments on a set of established benchmarks show that our tool is almost always faster than the state of the art, often by orders of magnitude, and was also able to synthesize an entire TLA+protocol “from scratch” in less than 3 minutes where the state of the art timed out after an hour. Our method is sound, complete, and guaranteed to terminate on unrealizable synthesis instances under common assumptions which hold in all our benchmarks.
more »
« less
- Award ID(s):
- 2319500
- PAR ID:
- 10614495
- Publisher / Repository:
- Springer Nature Switzerland
- Date Published:
- ISSN:
- 978-3-031-90653-4
- ISBN:
- 978-3-031-90652-7
- Page Range / eLocation ID:
- 155 to 176
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
null (Ed.)Syntax-guided synthesis (SyGuS) aims to find a program satisfying semantic specification as well as user-provided structural hypotheses. There are two main synthesis approaches: enumerative synthesis, which repeatedly enumerates possible candidate programs and checks their correctness, and deductive synthesis, which leverages a symbolic procedure to construct implementations from specifications. Neither approach is strictly better than the other: automated deductive synthesis is usually very efficient but only works for special grammars or applications; enumerative synthesis is very generally applicable but limited in scalability. In this paper, we propose a cooperative synthesis technique for SyGuS problems with the conditional linear integer arithmetic (CLIA) background theory, as a novel integration of the two approaches, combining the best of the two worlds. The technique exploits several novel divide-and-conquer strategies to split a large synthesis problem to smaller subproblems. The subproblems are solved separately and their solutions are combined to form a final solution. The technique integrates two synthesis engines: a pure deductive component that can efficiently solve some problems, and a height-based enumeration algorithm that can handle arbitrary grammar. We implemented the cooperative synthesis technique, and evaluated it on a wide range of benchmarks. Experiments showed that our technique can solve many challenging synthesis problems not possible before, and tends to be more scalable than state-of-the-art synthesis algorithms.more » « less
-
Abstract We present a comprehensive statistical analysis of high‐frequency transient‐large‐amplitude (TLA) magnetic perturbation events that occurred at 12 high‐latitude ground magnetometer stations throughout Solar Cycle 24 from 2009 to 2019. TLA signatures are defined as one or more second‐timescale dB/dtinterval with magnitude ≥6 nT/s within an hour event window. This study characterizes high‐frequency TLA events based on their spatial and temporal behavior, relation to ring current activity, auroral substorms, and nighttime geomagnetic disturbance (GMD) events. We show that TLA events occur primarily at night, solely in the high‐latitude region above 60° geomagnetic latitude, and commonly within 30 min of substorm onsets. The largest TLA events occurred more often in the declining phase of the solar cycle when ring current activity was lower and solar wind velocity was higher, suggesting association to high‐speed streams caused by coronal holes and subsequent corotating interaction regions reaching Earth. TLA perturbations often occurred preceding or within the most extreme nighttime GMD events that have 5–10 min timescales, but the TLA intervals were often even more localized than the ∼300 km effective scale size of GMDs. We provide evidence that shows TLA‐related GMD events are associated with dipolarization fronts in the magnetotail and fast flows toward Earth and are closely temporally associated with poleward boundary intensifications (PBIs) and auroral streamers. The highly localized behavior and connection to the most extreme GMD events suggests that TLA intervals are a ground manifestation of features within rapid and complex ionospheric structures that can drive geomagnetically induced currents.more » « less
-
Abstract An extremely rapid process for self‐assembling well‐ordered, nano, and microparticle monolayers via a novel aerosolized method is presented. The novel technique can reach monolayer self‐assembly rates as high as 268 cm2min−1from a single aerosolizing source and methods to reach faster monolayer self‐assembly rates are outlined. A new physical mechanism describing the self‐assembly process is presented and new insights enabling high‐efficiency nanoparticle monolayer self‐assembly are developed. In addition, well‐ordered monolayer arrays from particles of various sizes, surface functionality, and materials are fabricated. This new technique enables a 93× increase in monolayer self‐assembly rates compared to the current state of the art and has the potential to provide an extremely low‐cost option for submicron nanomanufacturing.more » « less
-
Abstract Objective.Invasive brain–computer interfaces (BCIs) have shown promise in restoring motor function to those paralyzed by neurological injuries. These systems also have the ability to restore sensation via cortical electrostimulation. Cortical stimulation produces strong artifacts that can obscure neural signals or saturate recording amplifiers. While front-end hardware techniques can alleviate this problem, residual artifacts generally persist and must be suppressed by back-end methods.Approach.We have developed a technique based on pre-whitening and null projection (PWNP) and tested its ability to suppress stimulation artifacts in electroencephalogram (EEG), electrocorticogram (ECoG) and microelectrode array (MEA) signals from five human subjects.Main results.In EEG signals contaminated by narrow-band stimulation artifacts, the PWNP method achieved average artifact suppression between 32 and 34 dB, as measured by an increase in signal-to-interference ratio. In ECoG and MEA signals contaminated by broadband stimulation artifacts, our method suppressed artifacts by 78%–80% and 85%, respectively, as measured by a reduction in interference index. When compared to independent component analysis, which is considered the state-of-the-art technique for artifact suppression, our method achieved superior results, while being significantly easier to implement.Significance.PWNP can potentially act as an efficient method of artifact suppression to enable simultaneous stimulation and recording in bi-directional BCIs to biomimetically restore motor function.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript
- Book Chapter:
- https://doi.org/10.1007/978-3-031-90653-4_8
