A5090498111- Formal Methods in Verification
- Logic, programming, and type systems
- Distributed systems and fault tolerance
- Logic, Reasoning, and Knowledge
- Gene Regulatory Network Analysis
- Model-Driven Software Engineering Techniques
- Advanced Software Engineering Methodologies
- Computational Drug Discovery Methods
- Service-Oriented Architecture and Web Services
- Advanced Authentication Protocols Security
- Petri Nets in System Modeling
- Semantic Web and Ontologies
- Bioinformatics and Genomic Networks
- Advanced Database Systems and Queries
- Distributed and Parallel Computing Systems
- User Authentication and Security Systems
- Security and Verification in Computing
- Multi-Agent Systems and Negotiation
- Embedded Systems Design Techniques
- Biomedical Text Mining and Ontologies
- Parallel Computing and Optimization Techniques
- Real-Time Systems Scheduling
- Microbial Metabolic Engineering and Bioproduction
- Computability, Logic, AI Algorithms
- Cryptographic Implementations and Security
SRI International
2015-2024
Menlo School
2014-2023
RWTH Aachen University
2022
Clausthal University of Technology
2022
Inria Saclay - Île de France
2022
Université Paris-Saclay
2022
Boeing (United States)
2022
University of California, Irvine
2012-2022
Centre National de la Recherche Scientifique
2022
American Jewish Committee
2022
We present an actor language which is extension of a simple functional language, and provide operational semantics for this extension. Actor configurations represent open distributed systems, by we mean that the specification system explicitly takes into account interface with external components. study composability such systems. define various notions testing equivalence on expressions configurations. The model develop provides fairness. An important result three forms equivalence, namely,...
We present ADDSEN middleware as a holistic solution for Adaptive Data processing and dissemination Drone swarms in urban SENsing. To efficiently process sensed data the middleware, we have proposed cyber-physical sensing framework using partially ordered knowledge sharing distributed management drone swarms. A reinforcement learning strategy is implemented framework. uses online techniques to adaptively balance broadcast rate loss periodically. The learned adapted by executing state...
Background Chagas disease is a neglected tropical (NTD) caused by the eukaryotic parasite Trypanosoma cruzi. The current clinical and preclinical pipeline for T. cruzi extremely sparse lacks drug target diversity. Methodology/Principal Findings In present study we developed computational approach that utilized data from several public whole-cell, phenotypic high throughput screens have been completed Broad Institute, including single screen of over 300,000 molecules in search chemical probes...
Abstract Traditionally the view has been that direct expression of control and store mechanisms clear mathematical semantics are incompatible requirements. This paper shows adding objects with memory to call-by-value lambda calculus results in a language rich equational theory, satisfying many usual laws. Combined other recent work, this provides evidence expressive, mathematically clean programming languages indeed possible.
The E.S.R. spectra of the radical anions pyridine, 4-picoline, 3,5-lutidine, 2,6-lutidine, pyrazine, pyrimidine, pyridine N-oxide, 4-picoline N-oxide and 2,6-lutidine have been observed in liquid ammonia. data for pyrazine pyrimidine can be combined to evaluate Q N = +27·3, CN -1·7 H -24·5 gauss independently molecular orbital spin densities. Good agreement is found coupling constants N-heterocyclics McLachlan's theory with methyl group consistent both Levy's hyperconjugation equations CH3...
We propose a formal model for reputation-based trust management. In contrast to credential-based management, in our framework an agent's reputation serves as the basis trust. For example, access control policy may consider re
In this paper we describe the use of rewriting logic based Maude tool to model and analyze mammalian signaling pathways. We discuss representation underlying biological concepts events new search checking capabilities 2.0 modeled network. also Maude's reflective capability for meta modeling analyzing models themselves. The idea symbolic experiments opens up an exciting world challenging applications formal methods in general formalisms particular.
We present a new language for expressing policies that allow opportunistic spectrum access while not causing interference. CoRaL has expressive constructs numerical constraints, supports efficient reasoning, and will be verifiable. The is extensible so unanticipated policy types can encoded. also describe reasoner reasons about policies, show how this used with various cognitive radios (in case, an XG radio) to guarantee policy-specified behaviors allowing sharing.
Cancer is a heterogeneous disease resulting from the accumulation of genetic defects that negatively impact control cell division, motility, adhesion and apoptosis. Deregulation in signaling along EgfR-MAPK pathway common breast cancer, though manner which deregulation occurs varies between both individuals cancer subtypes.We were interested identifying subnetworks within are similarly deregulated across subsets cancers. To end, we mapped genomic, transcriptional proteomic profiles for 30...
In this paper we introduce a variable typed logic of effects inspired by the type systems Feferman for purely functional languages. VTLoE (Variable Typed Logic Effects) is introduced in two stages. The first stage first-order theory individuals built on assertions equality (operational equivalence à la Plotkin), and contextual assertions. second extends to include classes class membership. present provides an expressive language defining studying properties programs including program...
Abstract In this paper, we address the role of middleware in enabling robust and resilient cyber-physical systems (CPSs) future. particular, will focus on how adaptation services can be used to improve dependability instrumented based principles “computational reflection.” CPS environments incorporate a variety sensing actuation devices distributed architecture; such deployment is create digital representation evolving physical world its processes for use by broad range applications....
Interdomain routing stitches the disparate parts of Internet together, making protocol stability a critical issue to both researchers and practitioners. Yet, create safety proofs counterexamples by hand build simulators prototypes explore dynamics. Similarly, network operators analyze their router configurations manually or using homegrown tools. In this paper, we present comprehensive toolkit for analyzing implementing policies, ranging from high-level guidelines specific configurations....
This paper builds domain theoretic concepts upon an operational foundation. The basic theory consists of a single step reduction system from which ordering and equivalence on programs are defined. is then extended to include theory, including the notions directed set, least upper bound, complete partial order, monotonicity, continuity, finite element,ω-algebraicity, full abstraction, fixed point properties. We conclude by using these construct (strongly) fully abstract continuous model for...