Search

Compound flooding, where the combination or successive occurrence of two or more flood drivers leads to an extreme impact, can greatly exacerbate the adverse consequences associated with flooding in coastal regions. This paper reviews the practices and trends in coastal compound flood research methodologies and applications, as well as synthesizes key findings at regional and global scales. Systematic review is employed to construct a literature database of 271 studies relevant to compound flood hazards in a coastal context. This review explores the types of compound flood events, their mechanistic processes, and synthesizes the definitions and terms exhibited throughout the literature. Considered in the review are six flood drivers (fluvial, pluvial, coastal, groundwater, damming/dam failure, and tsunami) and five precursor events and environmental conditions (soil moisture, snow, temp/heat, fire, and drought). Furthermore, this review summarizes the trends in research methodology, examines the wide range of study applications, and considers the influences of climate change and urban environments. Finally, this review highlights the knowledge gaps in compound flood research and discusses the implications of review findings on future practices. Our five recommendations for future compound flood research are to: 1) adopt consistent definitions, terminology, and approaches; 2) expand the geographic coverage of research; 3) pursue more inter-comparison projects; 4) develop modelling frameworks that better couple dynamic earth systems; and 5) design urban and coastal infrastructure with compound flooding in mind. We hope this review will help to enhance understanding of compound flooding, guide areas for future research focus, and close knowledge gaps., Comment: 95 pages (Main Text 3-59, References 61-77, Appendix 77-95), 7 figures

Mental disorders may exhibit pathological brain rhythms and neurostimulation promises to alleviate of patients' symptoms by modifying these rhythms. Today, most neurostimulation schemes are open-loop, i.e. administer experimental stimulation protocols independent of the patients brain activity which may yield a sub-optimal treatment. We propose a closed-loop feedback control scheme estimating an optimal stimulation based on observed brain activity. The optimal stimulation is chosen according to a user-defined target frequency distribution, which permits frequency tuning of the brain activity in real-time. The mathematical description details the major control elements and applications to biologically realistic simulated brain activity illustrate the scheme's possible power in medical practice. Clinical relevance - The proposed neurostimulation control theme promises to permit the medical personnel to tune a patient's brain activity in real-time.

Mental disorders (MD) are among the top most demanding challenges in world-wide health. According to the World Health Organization, the burden of MDs continues to grow with significant impact on health and major social and human rights. A large number of MDs exhibit pathological rhythms, which serve as the disorders characteristic biomarkers. These rhythms are the targets for neurostimulation techniques. Open-loop neurostimulation employs stimulation protocols, which are rather independent of the patients health and brain state in the moment of treatment. Most alternative closed-loop stimulation protocols consider real-time brain activity observations but appear as adaptive open-loop protocols, where e.g. pre-defined stimulation sets in if observations fulfil pre-defined criteria. The present theoretical work proposes a fully-adaptive closed-loop neurostimulation setup, that tunes the brain activities power spectral density (PSD) according to a user-defined PSD. The utilized brain model is non-parametric and estimated from the observations via magnitude fitting in a pre-stimulus setup phase. Moreover, the algorithm takes into account possible conduction delays in the feedback connection between observation and stimulation electrode. All involved features are illustrated on pathological alpha- and gamma-rhythms known from psychosis. To this end, we simulate numerically a linear neural population brain model and a non-linear cortico-thalamic feedback loop model recently derived to explain brain activity in psychosis.

Neural Networks are used today in numerous security- and safety-relevant domains and are, as such, a popular target of attacks that subvert their classification capabilities, by manipulating the network parameters. Prior work has introduced sensitive samples -- inputs highly sensitive to parameter changes -- to detect such manipulations, and proposed a gradient ascent-based approach to compute them. In this paper we offer an alternative, using symbolic constraint solvers. We model the network and a formal specification of a sensitive sample in the language of the solver and ask for a solution. This approach supports a rich class of queries, corresponding, for instance, to the presence of certain types of attacks. Unlike earlier techniques, our approach does not depend on convex search domains, or on the suitability of a starting point for the search. We address the performance limitations of constraint solvers by partitioning the search space for the solver, and exploring the partitions according to a balanced schedule that still retains completeness of the search. We demonstrate the impact of the use of solvers in terms of functionality and search efficiency, using a case study for the detection of Trojan attacks on Neural Networks., Comment: In Proceedings SCSS 2021, arXiv:2109.02501

We consider the broad problem of analyzing safety properties of asynchronous concurrent programs under arbitrary thread interleavings. Delay-bounded deterministic scheduling, introduced in prior work, is an efficient bug-finding technique to curb the large cost associated with full scheduling nondeterminism. In this paper we first present a technique to lift the delay bound for the case of finite-domain variable programs, thus adding to the efficiency of bug detection the ability to prove safety of programs under arbitrary thread interleavings. Second, we demonstrate how, combined with predicate abstraction, our technique can both refute and verify safety properties of programs with unbounded variable domains, even for unbounded thread counts. Previous work has established that, for non-trivial concurrency routines, predicate abstraction induces a highly complex abstract program semantics. Our technique, however, never statically constructs an abstract parametric program; it only requires some abstract-states set to be closed under certain actions, thus eliminating the dependence on the existence of verification algorithms for abstract programs. We demonstrate the efficiency of our technique on many examples used in prior work, and showcase its simplicity compared to earlier approaches on the unbounded-thread Ticket Lock protocol., Comment: This is an extended technical report of a paper published in CAV 2021

We address the problem of analyzing asynchronous event-driven programs, in which concurrent agents communicate via unbounded message queues. The safety verification problem for such programs is undecidable. We present in this paper a technique that combines queue-bounded exploration with a convergence test: if the sequence of certain abstractions of the reachable states, for increasing queue bounds k, converges, we can prove any property of the program that is preserved by the abstraction. If the abstract state space is finite, convergence is guaranteed; the challenge is to catch the point k_max where it happens. We further demonstrate how simple invariants formulated over the concrete domain can be used to eliminate spurious abstract states, which otherwise prevent the sequence from converging. We have implemented our technique for the P programming language for event-driven programs. We show experimentally that the sequence of abstractions often converges fully automatically, in hard cases with minimal designer support in the form of sequentially provable invariants, and that this happens for a value of k_max small enough to allow the method to succeed in practice., Comment: This is an extended technical report of a paper published in CAV 2019

A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is undecidable. A technique proposed by Qadeer and Rehof, to bound the number of context switches allowed between the threads, leads to an incomplete solution that is, however, believed to catch "most bugs" in practice. The question whether the technique can also prove the absence of bugs at least in some cases has remained largely open. In this paper we introduce a broad verification methodology for resource-parameterized programs that observes how changes to the resource parameter affect the behavior of the program. Applied to the context-unbounded analysis problem (CUBA), the methodology results in partial verification techniques for procedural concurrent programs. Our solutions may not terminate, but are able to both refute and prove context-unbounded safety for concurrent recursive threads. We demonstrate the effectiveness of our method using a variety of examples, the safe of which cannot be proved safe by earlier, context-bounded methods., Comment: 16 pages

Exploration algorithms for explicit-state transition systems are a core back-end technology in program verification. They can be applied to programs by generating the transition system on the fly, avoiding an expensive up-front translation. An on-the-fly strategy requires significant modifications to the implementation, into a form that stores states directly as valuations of program variables. Performed manually on a per-algorithm basis, such modifications are laborious and error-prone. In this paper we present the IJIT Application Programming Interface (API), which allows users to automatically transform a given transition system exploration algorithm to one that operates on Boolean programs. The API converts system states temporarily to program states just in time for expansion via image computations, forward or backward. Using our API, we have effortlessly extended various non-trivial (e.g. infinite-state) model checking algorithms to operate on multi-threaded Boolean programs. We demonstrate the ease of use of the API, and present a case study on the impact of the just-in-time translation on these algorithms., Comment: The 15th International Conference on Software Engineering and Formal Methods (SEFM 2017)

We present a method for accelerating explicit-state backward search algorithms for systems of arbitrarily many finite-state threads. Our method statically analyzes the program executed by the threads for the existence of simple loops. We show how such loops can be collapsed without approximation into Presburger arithmetic constraints that symbolically summarize the effect of executing the backward search algorithm along the loop in the multi-threaded program. As a result, the subsequent explicit-state search does not need to explore the summarized part of the state space. The combination of concrete and symbolic exploration gives our algorithm a concolic flavor. We demonstrate the power of this method for proving and refuting safety properties of unbounded-thread programs., Comment: arXiv admin note: substantial text overlap with arXiv:1505.02637

We present an approach to parameterized reachability for communicating finite-state threads that formulates the analysis as a satisfiability problem. In addition to the unbounded number of threads, the main challenge for SAT/SMT-based reachability methods is the existence of unbounded loops in the program executed by a thread. We show in this paper how simple loops can be accelerated without approximation into Presburger arithmetic constraints. The constraints are obtained via symbolic execution and are satisfiable exactly if the given program state is reachable. We summarize loops nested inside other loops using recurrence relations derived from the inner loop's acceleration. This summary abstracts the loop iteration parameter and may thus overapproximate. An advantage of our symbolic approach is that the process of building the Presburger formulas may instantly reveal their unsatisfiability, before any arithmetic has been performed. We demonstrate the power of this technique for proving and refuting safety properties of unbounded-thread programs and other infinite-state transition systems.

Monotonicity in concurrent systems stipulates that, in any global state, extant system actions remain executable when new processes are added to the state. This concept is not only natural and common in multi-threaded software, but also useful: if every thread's memory is finite, monotonicity often guarantees the decidability of safety property verification even when the number of running threads is unknown. In this paper, we show that the act of obtaining finite-data thread abstractions for model checking can be at odds with monotonicity: Predicate-abstracting certain widely used monotone software results in non-monotone multi-threaded Boolean programs - the monotonicity is lost in the abstraction. As a result, well-established sound and complete safety checking algorithms become inapplicable; in fact, safety checking turns out to be undecidable for the obtained class of unbounded-thread Boolean programs. We demonstrate how the abstract programs can be modified into monotone ones, without affecting safety properties of the non-monotone abstraction. This significantly improves earlier approaches of enforcing monotonicity via overapproximations.