A5053852359- Formal Methods in Verification
- Software Testing and Debugging Techniques
- Software Reliability and Analysis Research
- Explainable Artificial Intelligence (XAI)
- Bayesian Modeling and Causal Inference
- Logic, programming, and type systems
- Adversarial Robustness in Machine Learning
- Software Engineering Research
- Logic, Reasoning, and Knowledge
- Machine Learning and Data Classification
- Embedded Systems Design Techniques
- Machine Learning and Algorithms
- semigroups and automata theory
- Security and Verification in Computing
- Advanced Causal Inference Techniques
- Reinforcement Learning in Robotics
- Philosophy and History of Science
- Distributed systems and fault tolerance
- Data Stream Mining Techniques
- Radiomics and Machine Learning in Medical Imaging
- Cell Image Analysis Techniques
- Parallel Computing and Optimization Techniques
- Complexity and Algorithms in Graphs
- Model-Driven Software Engineering Techniques
- Radiation Effects in Electronics
King's College London
2015-2024
IBM Research - Haifa
2005-2017
Cornell University
2017
The King's College
2013
IBM (United States)
2006-2012
Mount Carmel Health
2007-2011
Carmel (Israel)
2006-2009
University of Haifa
2006-2009
Worcester Polytechnic Institute
2005
Massachusetts Institute of Technology
2005
Causality is typically treated an all-or-nothing concept; either A a cause of B or it not. We extend the definition causality introduced by Halpern and Pearl [2004a] to take into account degree responsibility for B. For example, if someone wins election 11-0, then each person who votes him less responsible victory than he had won 6-5. define notion blame, which takes agent's epistemic state. Roughly speaking, blame expected B, taken over state agent.
As cloud-based services gain popularity in both private and enterprise domains, cloud consumers are still lacking tools to verify that these work as expected. Such should consider properties such functional correctness, service availability, reliability, performance security guarantees. In this paper we survey existing areas identify gaps technology terms of the verification provided users. We also discuss challenges new research directions can help bridge gaps.
Even when a system is proven to be correct with respect specification, there still question of how complete the specification is, and whether it really covers all behaviors system. Coverage metrics attempt check which parts are actually relevant for verification process succeed. Recent work on coverage in model checking suggests several algorithms finding that not covered by specification. The has already effective practice, detecting design errors escape early efforts industrial settings....
Formal verification is a reliable and fully automatic technique for proving correctness of hardware designs. Its main drawback the high complexity verification, this problem especially acute in regression where new version design, differing from previous very slightly, verified with respect to same or similar property. In paper, we present an efficient algorithm incremental based on ic3 algorithm, that uses stored information runs order improve re-verifying designs properties. Our applies...
In formal verification, we verify that a system is correct with respect to specification. Cases like antecedent failure can make successful pass of the verification procedure meaningless. Vacuity detection signal such "meaningless" passes specification, and indeed vacuity checks are now standard component in many commercial model checkers. We address two dimensions vacuity: computational effort information given user. As for first dimension, present several preliminary be done without design...
An important challenge in the field of law is attribution responsibility and blame to individuals organisations for a given harm. Attributing legal often involves (but not limited to) assessing what extent certain parties have caused harm, or could prevented harm from occurring. This paper presents causal framework performing such assessments that particularly suitable analysis complex cases, where actions many had direct indirect effect on did occur. evaluated by means case study applies it...
Coverage is a means to quantify the quality of system specification, and frequently applied assess progress in validation. standard measure testing, but very difficult compute context formal verification. We present efficient algorithms for identifying those parts that are covered by given property. Our algorithm integrated into state-of-the-art SAT-based Model Checking using Craig interpolation. The key insight our re-use previously computed inductive invariants counterexamples. This...