A5075576417- Formal Methods in Verification
- Software Testing and Debugging Techniques
- VLSI and Analog Circuit Testing
- Embedded Systems Design Techniques
- Model-Driven Software Engineering Techniques
- Radiation Effects in Electronics
- Dermatologic Treatments and Research
- Facial Rejuvenation and Surgery Techniques
- Physical Unclonable Functions (PUFs) and Hardware Security
- Advanced Malware Detection Techniques
- Software Reliability and Analysis Research
- Security and Verification in Computing
- Safety Systems Engineering in Autonomy
- Petri Nets in System Modeling
- Botulinum Toxin and Related Neurological Disorders
- Information and Cyber Security
- Diverse Legal and Medical Studies
- Adversarial Robustness in Machine Learning
- Advanced Software Engineering Methodologies
- Software Engineering Research
- Artificial Intelligence in Healthcare and Education
- Flexible and Reconfigurable Manufacturing Systems
- Medical and Health Sciences Research
- Interconnection Networks and Systems
- Body Contouring and Surgery
Télécom Paris
2018-2022
Messer (Germany)
2014-2021
Laboratoire Traitement et Communication de l’Information
2018-2021
Université Paris-Saclay
2018
Leipzig/Halle Airport
2012-2018
University of Bremen
2006-2016
École Normale Supérieure Paris-Saclay
2011-2015
École Normale Supérieure
2015
Staats- und Universitätsbibliothek Bremen
2013
Centre National de la Recherche Scientifique
2011
Formal verification utilizing symbolic computer algebra has demonstrated the ability to formally verify large Galois field arithmetic circuits and basic architectures of integer circuits.The technique models circuit as Gröbner basis polynomials reduces polynomial equation specification wrt. model.However, during reduction, suffers from exponential blow-up in size polynomials, if it is applied on parallel adders recoded multipliers.In this paper, we address reasons present an approach that...
This paper documents how an ethically aligned co-design methodology ensures trustworthiness in the early design phase of artificial intelligence (AI) system component for healthcare. The explains decisions made by deep learning networks analyzing images skin lesions. trustworthy AI developed here used a holistic approach rather than static ethical checklist and required multidisciplinary team experts working with designers their managers. Ethical, legal, technical issues potentially arising...
Artificial Intelligence (AI) has the potential to greatly improve delivery of healthcare and other services that advance population health wellbeing. However, use AI in also brings risks may cause unintended harm. To guide future developments AI, High-Level Expert Group on set up by European Commission (EC), recently published ethics guidelines for what it terms “trustworthy” AI. These are aimed at a variety stakeholders, especially guiding practitioners toward more ethical robust...
This article's main contributions are twofold: 1) to demonstrate how apply the general European Union's High-Level Expert Group's (EU HLEG) guidelines for trustworthy AI in practice domain of healthcare and 2) investigate research question what does "trustworthy AI" mean at time COVID-19 pandemic. To this end, we present results a post-hoc self-assessment evaluate trustworthiness an system predicting multiregional score conveying degree lung compromise patients, developed verified by...
Following the trend in facial cosmetic procedures, patients are now increasingly requesting hand rejuvenation treatments. Intrinsic ageing of hands is characterized by loss dermal elasticity and atrophy subcutaneous tissue. Thus, veins, tendons bony structures become apparent. Among available intrinsic best improved restoring volume soft Volume restoration can be achieved with a number long-lasting fillers varying degrees improvement treatment longevity. The used include autologous fat,...
Today, the underlying hardware of embedded systems is often verified successfully. In this context formal verification techniques allow to prove functional correctness. But in system design integration software components becomes more and important. paper we present an integrated approach for software. The demonstrated on a RISC CPU. based bounded model checking. Besides correctness proofs hardware/software interface programs using can be formally verified.
Due to high computational costs of formal verification on pure Boolean level, proof techniques the word like Satisfiability Modulo Theories (SMT), were proposed. Verification methods originally based satisfiability (SAT) can directly benefit from this progress. In work we present level framework WoLFram that enables development applications for systems independent underlying technique. The is partitioned into an application layer, a core engine and back-end layer. A wide range implemented,...
<para xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"> Formal verification is an important issue in circuit and system design. In this context, bounded model checking (BMC) one of the most successful techniques. However, even if all specified properties can be verified, it difficult to determine whether they cover complete functional behavior a We propose practical approach analyze coverage BMC. The easily integrated BMC tool with only minor changes....
Equivalence checking and property are powerful techniques to detect error traces. Debugging these traces is a time consuming design task where automation provides help. In particular, debugging based on Boolean Satisfiability (SAT) has been shown be quite efficient. Given some traces, the algorithm returns fault candidates. But using random cannot ensure that candidate sufficient explain all erroneous behaviors. Our approach more accurate diagnosis by iterating generation of counterexamples...
The complexity of today's embedded and cyber-physical systems is rapidly increasing makes the consideration higher levels abstraction during design process inevitable. In this context, impact modeling languages such as UML its profiles MARTE growing. Here, CCSL provides a formal description timing constraints which have to be enforced on considered system. This builds basis for many further steps can used e. g. checking consistency specification, code generation, or proving whether time...
Equivalence checking and property are powerful techniques to detect error traces. Debugging these traces is a time consuming design task where automation provides help. In particular, debugging based on Boolean satisfiability (SAT) has been shown be quite efficient. Given some traces, the algorithm returns fault candidates. But using random cannot ensure that candidate sufficient explain all erroneous behaviors. Our approach more accurate diagnosis by iterating generation of counterexamples...
Formal verification is an important issue in circuit and system design. In this context, Bounded Model Checking (BMC) one of the most successful techniques. But even if all specified properties can be verified, it difficult to determine whether they cover complete functional behavior a We propose pragmatic approach estimate coverage BMC. The easily integrated BMC tool with only minor changes. our approach, property generated for each signal. If considered do not describe signal's entire...
The application of built-to-order embedded hardware designs in safety critical systems requires a high design quality and robustness during operation. Flawless execution the involved software can be compromised by malfunctioning components or software-induced errors. Furthermore, intellectual property (IP) tends to become unavoidable modern designs. Any unexpected behavior IP may cause unrecoverable system In order construct correct safe from unverified potentially malicious components, we...
Cohesive polydensified matrix (CPM®) hyaluronic acid fillers are now available with or without lidocaine. The aim of this study was to investigate the safety and performance CPM® lidocaine in clinical setting. In an open-label, prospective, postmarketing study, 108 patients from seven sites Germany Denmark were treated one more lidocaine-containing fillers. Performance assessed using Merz Aesthetics Scales® (MAS). Pain rated on 11-point visual analog scale. Patients' physicians' satisfaction...
Formal verification is an important issue in circuit and system design. In this context, bounded model checking (BMC) one of the most successful techniques. But even if all specified properties can be verified, it difficult to determine whether they cover complete functional behavior a We propose pragmatic approach estimate coverage BMC. The easily integrated BMC tool with only minor changes. our approach, property generated for each signal. If considered do not describe signal's entire...
In this paper we present a hardware based solution to verify simultaneously Code and Control-Flow Integrity (CCFI), aiming at protecting microcontrollers against both cyber-and physical attacks. This is non-intrusive as it does not require any modification of the CPU core. It relies on two additional blocks external CPU: The first one – called CCFI-cache acts dedicated cache for storage information check code control-flow integrity, second CCFI-checker performs integrity verification. Based...
To keep up with the growing complexity of digital systems, high level models are used in design process. In today's processor design, a comprehensive tool chain can be built automatically from architectural or transaction models, but disregarding formal verification. We present an approach to generate complete property suite architecture description, that formally verify register transfer (RTL) implementation processor. The is by construction, i.e. exhaustive verification all functionality...
Today for System-on-Chips (SoCs) companies Electronic System Level(ESL) design is the established approach. Abstraction and standardized communication interfaces based on SystemC Transaction Level Modeling (TLM) have become core component ESL design. The abstract models in flows are stepwise refined down to hardware. In this context verification major bottleneck: After each refinement step resulting model simulated again with same testbench. simulation results be compared previous check...