A5051084250- Formal Methods in Verification
- Logic, programming, and type systems
- Software Testing and Debugging Techniques
- Security and Verification in Computing
- Logic, Reasoning, and Knowledge
- Multi-Agent Systems and Negotiation
- Access Control and Trust
- Model-Driven Software Engineering Techniques
- Advanced Software Engineering Methodologies
- Privacy, Security, and Data Protection
- Privacy-Preserving Technologies in Data
- Diverse Scientific and Economic Studies
- Distributed systems and fault tolerance
- Advanced Malware Detection Techniques
- Real-Time Systems Scheduling
- Business Process Modeling and Analysis
- Blockchain Technology Applications and Security
- Software Reliability and Analysis Research
- Semantic Web and Ontologies
- Cloud Data Security Solutions
- Cryptography and Data Security
- Software Engineering Research
- Advanced Control Systems Optimization
- Software Engineering Techniques and Practices
- Service-Oriented Architecture and Web Services
Chalmers University of Technology
2014-2024
University of Gothenburg
2015-2024
Norwegian University of Science and Technology
2022
Karlstad University
2022
Göteborgs Stads
2016
University of Oslo
2005-2013
Universidad Nacional de Entre Ríos
2013
Infor (Norway)
2007
Institut de Recherche en Informatique et Systèmes Aléatoires
2005
Centre National de la Recherche Scientifique
2004-2005
The use of runtime verification, as a lightweight approach to guarantee properties systems, has been increasingly employed on real-life software. In this paper, we present the tool LARVA, for verification Java programs, including real-time properties. Properties can be expressed in number notations, timed-automata enriched with stopwatches, Lustre, and subset duration calculus. successfully used case-studies, an industrial system handling financial transactions. LARVA also performs analysis...
Abstract Runtime verification is an area of formal methods that studies the dynamic analysis execution traces against specifications. Typically, two main activities in runtime efforts are process creating monitors from specifications, and algorithms for evaluation generated monitors. Other involve instrumentation system to generate trace communication between under monitor. Most applications have been focused on software, even though there many more potential other computational devices...
Differential privacy provides a way to get useful information about sensitive data without revealing much any one individual. It enjoys many nice compositionality properties not shared by other approaches privacy, including, in particular, robustness against side-knowledge.
Static verification techniques are used to analyse and prove properties about programs before they executed. Many of these work directly on the source code verify data-oriented over all possible executions. The analysis is necessarily an over-approximation as real executions program not available at time. In contrast, runtime have been extensively for control-oriented properties, analysing current execution path in a fully automatic manner. this article, we present novel approach which may...
Differential privacy provides a way to get useful information about sensitive data without revealing much any one individual. It enjoys many nice compositionality properties not shared by other approaches privacy, including, in particular, robustness against side-knowledge. Designing differentially private mechanisms from scratch can be challenging task. One make it easier construct new differential is design system which allows more complex (programs) built building blocks principled way,...
Due to the upcoming, more restrictive regulations (like European GDPR), designing privacy preserving architectures for information systems is becoming a pressing concern practitioners. In particular, verifying that design compliant with might be challenging task engineers. This work presents an approach based on model transformations, which guarantee architectural encompasses regulation-oriented principles such as purpose limitation, or accountability of data controller. Our improves state...
In a web service composition, an electronic contract (e-contract) regulates how the services participating in composition should behave, including restrictions that these must fulfill, such as real-time constraints. this work we present visual model allows us to specify e-contracts user friendly way, conditional behavior and realtime A case study is presented illustrate defines preliminary evaluation of also done.