A5087431438- Formal Methods in Verification
- Logic, programming, and type systems
- Distributed systems and fault tolerance
- Model-Driven Software Engineering Techniques
- Software Testing and Debugging Techniques
- Parallel Computing and Optimization Techniques
- Petri Nets in System Modeling
- Security and Verification in Computing
- Advanced Malware Detection Techniques
- Web Application Security Vulnerabilities
- Fault Detection and Control Systems
- VLSI and Analog Circuit Testing
- Advanced Neural Network Applications
- Network Time Synchronization Technologies
- Real-Time Systems Scheduling
- Embedded Systems Design Techniques
- Computability, Logic, AI Algorithms
- Advanced Software Engineering Methodologies
- semigroups and automata theory
- Adversarial Robustness in Machine Learning
- Software Engineering Research
- Natural Language Processing Techniques
- Cognitive Functions and Memory
- Machine Learning and Algorithms
- Mobile Agent-Based Network Management
Linköping University
2015-2024
Uppsala University
2005-2011
Université Paris Cité
2008-2009
Laboratoire d'Informatique Algorithmique: Fondements et Applications
2008-2009
Université Paris 8
2009
Informa (Sweden)
2006
Real-time communication over Ethernet is becoming important in various application areas of cyber-physical systems such as industrial automation and control, avionics, automotive networking. Since applications are typically time critical, technology has been enhanced to support time-driven through the IEEE 802.1 TSN standards. The performance stability control strongly impacted by timing network communication. Thus, order guarantee requirements, when synthesizing schedule routing, it needed...
We describe a uniform and efficient framework for checking the satisfiability of large class string constraints. The is based on observation that both unsatisfiability common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each which consists sequence loops. build Counter-Example Guided Abstraction Refinement (CEGAR) contains an under- over-approximation module. flow information between modules allows to increase...
We introduce TRAU, an SMT solver for expressive constraint language, including word equations, length constraints, context-free membership queries, and transducer constraints. The satisfiability problem such a class of constraints is in general undecidable. key idea behind TRAU technique called flattening, which searches satisfying assignments that follow simple patterns. implements Counter-Example Guided Abstraction Refinement (CEGAR) framework contains both under- over-approximation...
The interest in analyzing loosely connected and decentralized terrorist networks of global reach has grown during the past decade. Social Network Analysis (SNA) is one approach towards understanding since it can be used to analyze structure a network detect important persons links. In this work we study with different types nodes. nodes either organizations, places or persons. We use combination centrality measures key players such networks.
Cache timing attacks allow attackers to infer the properties of a secret execution by observing cache hits and misses. But how much information can actually leak through such attacks? For given program, model, an input, our CHALICE framework leverages symbolic compute amount that possibly attacks. At core is novel approach quantify highlight critical side-channel leaks on arbitrary binary code. In evaluation real-world programs from OpenSSL Linux GDK libraries, effectively quantifies leaks:...
Cache attacks allow attackers to infer the properties of a secret execution by observing cache hits and misses. But how much information can actually leak through such attacks? For given program, model, an input, our CHALICE framework leverages symbolic compute amount that possibly attacks. At core is novel approach quantify leakage highlight critical side-channel on arbitrary binary code. In evaluation real-world programs from OpenSSL Linux GDK libraries, effectively quantifies leakage:...
We introduce the simple and efficient method of monotonic abstraction to prove safety properties for parameterized systems with linear topologies. A process in system is a finite-state automaton, where transitions are guarded by both local global conditions. Processes may communicate via broadcast, rendez-vous shared variables over finite domains. The derives an over-approximation induced transition that allows use class regular expressions as symbolic representation. Compared traditional...
Generating functional tests for processors has been a challenging problem decades in the very large-scale integration testing field. This paper presents method that generates software-based self-tests by leveraging bounded model checking (BMC) techniques and targeting, first time, out-of-order [out-of-order execution (OOE)] superscalar processors. To combat state-space explosion associated with BMC, proposed starts combining module-level abstraction-refinement slicing to reduce size of under...