Jun Sun

Proceedings of the Fundamental Approaches to Software Engineering, 2021

Verification Assisted Gas Reduction for Smart Contracts.

[BibT_eX]

[DOI]

Proceedings of the 28th Asia-Pacific Software Engineering Conference, 2021

2020

Automated synthesis of local time requirement for service composition.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2020

Towards Repairing Neural Networks Correctly.

[BibT_eX]

[DOI]

CoRR, 2020

SOCRATES: Towards a Unified Platform for Neural Network Verification.

[BibT_eX]

[DOI]

Long H. Pham

Jiaying Li

CoRR, 2020

SAGA: Efficient and Large-Scale Detection of Near-Miss Clones with GPU Acceleration.

[BibT_eX]

[DOI]

Proceedings of the 27th IEEE International Conference on Software Analysis, 2020

Systematic Classification of Attackers via Bounded Model Checking.

[BibT_eX]

[DOI]

Eric Rothstein Morris

Sudipta Chattopadhyay

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2020

Semantic Understanding of Smart Contracts: Executable Operational Semantics of Solidity.

[BibT_eX]

[DOI]

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Accelerating All-SAT Computation with Short Blocking Clauses.

[BibT_eX]

[DOI]

Yueling Zhang

Geguang Pu

Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020

Towards Generating Thread-Safe Classes Automatically.

[BibT_eX]

[DOI]

Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020

Towards Interpreting Recurrent Neural Networks through Probabilistic Abstraction.

[BibT_eX]

[DOI]

Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, 2020

ObjSim: efficient testing of cyber-physical systems.

[BibT_eX]

[DOI]

Zijiang Yang

Proceedings of the ISSTA '20: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2020

Active fuzzing for testing and securing cyber-physical systems.

[BibT_eX]

[DOI]

Bohan Xuan

Fan Zhang

Proceedings of the ISSTA '20: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2020

Recovering fitness gradients for interprocedural Boolean flags in search-based testing.

[BibT_eX]

[DOI]

Proceedings of the ISSTA '20: 29th ACM SIGSOFT International Symposium on Software Testing and Analysis, 2020

What Makes Open Source Software Projects Impactful: A Data-Driven Approach.

[BibT_eX]

[DOI]

Proceedings of the Internetware'20: 12th Asia-Pacific Symposium on Internetware, 2020

White-box fairness testing through adversarial sampling.

[BibT_eX]

[DOI]

Proceedings of the ICSE '20: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June, 2020

Symbolic verification of message passing interface programs.

[BibT_eX]

[DOI]

Proceedings of the ICSE '20: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June, 2020

sFuzz: an efficient adaptive fuzzer for solidity smart contracts.

[BibT_eX]

[DOI]

Proceedings of the ICSE '20: 42nd International Conference on Software Engineering, Seoul, South Korea, 27 June, 2020

Learning Fault Models of Cyber Physical Systems.

[BibT_eX]

[DOI]

Teck Ping Khoo

Sudipta Chattopadhyay

Proceedings of the Formal Methods and Software Engineering, 2020

IFIX: Fixing Concurrency Bugs While They Are Introduced.

[BibT_eX]

[DOI]

Proceedings of the 25th International Conference on Engineering of Complex Computer Systems, 2020

Automatic Verification of Multi-threaded Programs by Inference of Rely-Guarantee Specifications.

[BibT_eX]

[DOI]

Proceedings of the 25th International Conference on Engineering of Complex Computer Systems, 2020

An Empirical Study on Correlation between Coverage and Robustness for Deep Neural Networks.

[BibT_eX]

[DOI]

Proceedings of the 25th International Conference on Engineering of Complex Computer Systems, 2020

A Generalized Formal Semantic Framework for Smart Contracts.

[BibT_eX]

[DOI]

Jiao Jiao

Shang-Wei Lin

Proceedings of the Fundamental Approaches to Software Engineering, 2020

Provably Robust Decisions based on Potentially Malicious Sources of Information.

[BibT_eX]

[DOI]

Tim Muller

Dongxia Wang

Proceedings of the 33rd IEEE Computer Security Foundations Symposium, 2020

Global PAC Bounds for Learning Discrete Time Markov Chains.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 32nd International Conference, 2020

CoinWatch: A Clone-Based Approach For Detecting Vulnerabilities in Cryptocurrencies.

[BibT_eX]

[DOI]

Proceedings of the IEEE International Conference on Blockchain, 2020

2019

Sequential Schemes for Frequentist Estimation of Properties in Statistical Model Checking.

[BibT_eX]

[DOI]

Cyrille Jégourel

ACM Trans. Model. Comput. Simul., 2019

Practical static analysis of context leaks in Android applications.

[BibT_eX]

[DOI]

Flavio Toffalini

Martín Ochoa

Softw. Pract. Exp., 2019

There is Limited Correlation between Coverage and Robustness for Deep Neural Networks.

[BibT_eX]

[DOI]

CoRR, 2019

Analyzing Recurrent Neural Network by Probabilistic Abstraction.

[BibT_eX]

[DOI]

CoRR, 2019

AI-boosted software automation: learning from human pair programmers.

[BibT_eX]

[DOI]

Xin Peng

Zhenchang Xing

Sci. China Inf. Sci., 2019

Generative API usage code recommendation with parameter concretization.

[BibT_eX]

[DOI]

Sci. China Inf. Sci., 2019

Latent error prediction and fault localization for microservice applications by learning from system trace logs.

[BibT_eX]

[DOI]

Proceedings of the ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019

MAP-Coverage: A Novel Coverage Criterion for Testing Thread-Safe Classes.

[BibT_eX]

[DOI]

Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, 2019

Learning-Guided Network Fuzzing for Testing Cyber-Physical System Defences.

[BibT_eX]

[DOI]

Sridhar Adepu

Fan Zhang

Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, 2019

Adversarial sample detection for deep neural network through model mutation testing.

[BibT_eX]

[DOI]

Proceedings of the 41st International Conference on Software Engineering, 2019

sCompile: Critical Path Identification and Analysis for Smart Contracts.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2019

Adaptive Randomized Scheduling for Concurrency Bug Detection.

[BibT_eX]

[DOI]

Proceedings of the 24th International Conference on Engineering of Complex Computer Systems, 2019

Concolic Testing Heap-Manipulating Programs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - The Next 30 Years - Third World Congress, 2019

Careful-Packing: A Practical and Scalable Anti-Tampering Software Protection enforced by Trusted Computing.

[BibT_eX]

[DOI]

Proceedings of the Ninth ACM Conference on Data and Application Security and Privacy, 2019

Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2019

Parametric Timed Model Checking for Guaranteeing Timed Opacity.

[BibT_eX]

[DOI]

Étienne André

Proceedings of the Automated Technology for Verification and Analysis, 2019

Compositional Verification of Heap-Manipulating Programs Through Property-Guided Learning.

[BibT_eX]

[DOI]

Long H. Pham

Quang Loc Le

Proceedings of the Programming Languages and Systems - 17th Asian Symposium, 2019

2018

An Adaptive Markov Strategy for Defending Smart Grid False Data Injection From Malicious Attackers.

[BibT_eX]

[DOI]

IEEE Trans. Smart Grid, 2018

Towards Model Checking Android Applications.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2018

A Formal Specification and Verification Framework for Timed Security Protocols.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2018

CrowdService: Optimizing Mobile Crowdsourcing and Service Composition.

[BibT_eX]

[DOI]

ACM Trans. Internet Techn., 2018

Efficient and Robust Emergence of Norms through Heuristic Collective Learning.

[BibT_eX]

[DOI]

ACM Trans. Auton. Adapt. Syst., 2018

Learning probabilistic models for model checking: an evolutionary approach and an empirical study.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2018

Detecting Bitrate Modulation-Based Covert Voice-Over-IP Communication.

[BibT_eX]

[DOI]

IEEE Commun. Lett., 2018

A UTP semantics for communicating processes with shared variables and its formal encoding in PVS.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2018

Quantifying Attacker Capability Via Model Checking Multiple Properties (Extended Version).

[BibT_eX]

[DOI]

Eric Rothstein Morris

CoRR, 2018

sCompile: Critical Path Identification and Analysis for Smart Contracts.

[BibT_eX]

[DOI]

CoRR, 2018

Detecting Adversarial Samples for Deep Neural Networks through Mutation Testing.

[BibT_eX]

[DOI]

CoRR, 2018

Executable Operational Semantics of Solidity.

[BibT_eX]

[DOI]

CoRR, 2018

Frame Inference for Inductive Entailment Proofs in Separation Logic.

[BibT_eX]

[DOI]

Quang Loc Le

Shengchao Qin

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Learning from Mutants: Using Code Mutation to Learn and Monitor Invariants of a Cyber-Physical System.

[BibT_eX]

[DOI]

Proceedings of the 2018 IEEE Symposium on Security and Privacy, 2018

Delta debugging microservice systems.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

PFix: fixing concurrency bugs based on memory access patterns.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

Break the dead end of dynamic slicing: localizing data and control omission bug.

[BibT_eX]

[DOI]

Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 2018

On the Sequential Massart Algorithm for Statistical Model Checking.

[BibT_eX]

[DOI]

Cyrille Jégourel

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation. Verification, 2018

Benchmarking microservice systems for software engineering research.

[BibT_eX]

[DOI]

Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, 2018

Towards optimal concolic testing.

[BibT_eX]

[DOI]

Proceedings of the 40th International Conference on Software Engineering, 2018

Static analysis of context leaks in android applications.

[BibT_eX]

[DOI]

Flavio Toffalini

Martín Ochoa

Proceedings of the 40th International Conference on Software Engineering: Software Engineering in Practice, 2018

Testing heap-based programs with Java StarFinder.

[BibT_eX]

[DOI]

Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, 2018

The Miles Before Formal Methods - A Case Study on Modeling and Analyzing a Passenger Lift System.

[BibT_eX]

[DOI]

Teck Ping Khoo

Proceedings of the Formal Methods and Software Engineering, 2018

Compositional Reasoning for Shared-Variable Concurrent Programs.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 22nd International Symposium, 2018

Towards 'Verifying' a Water Treatment System.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods - 22nd International Symposium, 2018

Importance Sampling of Interval Markov Chains.

[BibT_eX]

[DOI]

Cyrille Jégourel

Jingyi Wang

Proceedings of the 48th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2018

2017

Language Inclusion Checking of Timed Automata with Non-Zenoness.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2017

Battery-Aware Mobile Data Service.

[BibT_eX]

[DOI]

IEEE Trans. Mob. Comput., 2017

Auditing Anti-Malware Tools by Evolving Android Malware and Dynamic Loading Technique.

[BibT_eX]

[DOI]

IEEE Trans. Inf. Forensics Secur., 2017

Detecting Steganography of Adaptive Multirate Speech with Unknown Embedding Rate.

[BibT_eX]

[DOI]

Mob. Inf. Syst., 2017

Hiding Information Into Voice-Over-IP Streams Using Adaptive Bitrate Modulation.

[BibT_eX]

[DOI]

IEEE Commun. Lett., 2017

Toward 'verifying' a Water Treatment System.

[BibT_eX]

[DOI]

Jingyi Wang

Yifan Jia

CoRR, 2017

Parametric Model Checking Timed Automata Under Non-Zenoness Assumption.

[BibT_eX]

[DOI]

Proceedings of the NASA Formal Methods - 9th International Symposium, 2017

O2O service composition with social collaboration.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

FiB: squeezing loop invariants by interpolation between Forward/Backward predicate transformers.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Mining implicit design templates for actionable code reuse.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

Automatic loop-invariant generation and refinement through selective sampling.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017

JSFox: integrating static and dynamic type analysis of JavaScript programs.

[BibT_eX]

[DOI]

Proceedings of the 39th International Conference on Software Engineering, 2017

Feedback-based debugging.

[BibT_eX]

[DOI]

Proceedings of the 39th International Conference on Software Engineering, 2017

Improving Probability Estimation Through Active Probabilistic Model Learning.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2017

Assertion Generation Through Active Learning.

[BibT_eX]

[DOI]

Long H. Pham

Lyly Tran Thi

Proceedings of the Formal Methods and Software Engineering, 2017

Classification-Based Parameter Synthesis for Parametric Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2017

A Verification Framework for Stateful Security Protocols.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2017

Learning Likely Invariants to Explain Why a Program Fails.

[BibT_eX]

[DOI]

Proceedings of the 22nd International Conference on Engineering of Complex Computer Systems, 2017

Anomaly Detection for a Water Treatment System Using Unsupervised Machine Learning.

[BibT_eX]

[DOI]

Jun Inoue

Yoriyuki Yamagata

Proceedings of the 2017 IEEE International Conference on Data Mining Workshops, 2017

Should We Learn Probabilistic Models for Model Checking? A New Approach and An Empirical Study.

[BibT_eX]

[DOI]

Proceedings of the Fundamental Approaches to Software Engineering, 2017

A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016

Improved EGT-Based Robustness Analysis of Negotiation Strategies in Multiagent Systems via Model Checking.

[BibT_eX]

[DOI]

IEEE Trans. Hum. Mach. Syst., 2016

Formalizing and verifying stochastic system architectures using Monterey Phoenix.

[BibT_eX]

[DOI]

Softw. Syst. Model., 2016

Compositional Reasoning for Shared-variable Concurrent Programs.

[BibT_eX]

[DOI]

CoRR, 2016

Verifying Complex Systems Probabilistically through Learning, Abstraction and Refinement.

[BibT_eX]

[DOI]

Jingyi Wang

Shengchao Qin

CoRR, 2016

IBED: Combining IBEA and DE for optimal feature selection in software product line engineering.

[BibT_eX]

[DOI]

Appl. Soft Comput., 2016

Regular Symmetry Patterns.

[BibT_eX]

[DOI]

Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2016

Designing minimal effective normative systems with the help of lightweight formal methods.

[BibT_eX]

[DOI]

Proceedings of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016

CrowdService: serving the individuals through mobile crowdsourcing and service composition.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, 2016

Optimizing selection of competing services with probabilistic hierarchical refinement.

[BibT_eX]

[DOI]

Proceedings of the 38th International Conference on Software Engineering, 2016

Scaling BDD-based Timed Verification with Simulation Reduction.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2016

Service Adaptation with Probabilistic Partial Models.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2016

Improving Quality of Use Case Documents through Learning and User Interaction.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Engineering of Complex Computer Systems, 2016

Towards Using Concurrent Java API Correctly.

[BibT_eX]

[DOI]

Proceedings of the 21st International Conference on Engineering of Complex Computer Systems, 2016

Automated Verification of Timed Security Protocols with Clock Drift.

[BibT_eX]

[DOI]

Li Li

Proceedings of the FM 2016: Formal Methods, 2016

Towards Concolic Testing for Hybrid Systems.

[BibT_eX]

[DOI]

Proceedings of the FM 2016: Formal Methods, 2016

Towards Learning and Verifying Invariants of Cyber-Physical Systems by Code Mutation.

[BibT_eX]

[DOI]

Proceedings of the FM 2016: Formal Methods, 2016

Satisfiability Modulo Heap-Based Programs.

[BibT_eX]

[DOI]

Quang Loc Le

Wei-Ngan Chin

Proceedings of the Computer Aided Verification - 28th International Conference, 2016

2015

A Systematic Study on Explicit-State Non-Zenoness Checking for Timed Automata.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2015

Regular Symmetry Patterns (Technical Report).

[BibT_eX]

[DOI]

CoRR, 2015

Event and Strategy Analytics.

[BibT_eX]

[DOI]

Proceedings of the 2015 International Symposium on Theoretical Aspects of Software Engineering, 2015

TLV: abstraction through testing, learning, and validation.

[BibT_eX]

[DOI]

Proceedings of the 2015 10th Joint Meeting on Foundations of Software Engineering, 2015

Formalizing and verifying stochastic system architectures using Monterey Phoenix (SoSyM abstract).

[BibT_eX]

[DOI]

Proceedings of the 18th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, 2015

Interpolation Guided Compositional Verification (T).

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering, 2015

Detection and classification of malicious JavaScript via attack behavior modelling.

[BibT_eX]

[DOI]

Mahinthan Chandramohan

Proceedings of the 2015 International Symposium on Software Testing and Analysis, 2015

Optimizing selection of competing features via feedback-directed evolutionary algorithms.

[BibT_eX]

[DOI]

Proceedings of the 2015 International Symposium on Software Testing and Analysis, 2015

Reliability assessment for distributed systems via communication abstraction and refinement.

[BibT_eX]

[DOI]

Proceedings of the 2015 International Symposium on Software Testing and Analysis, 2015

An Adaptive Markov Strategy for Effective Network Intrusion Detection.

[BibT_eX]

[DOI]

Jianye Hao

Yinxing Xue

Mahinthan Chandramohan

Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence, 2015

GPU Accelerated On-the-Fly Reachability Checking.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Engineering of Complex Computer Systems, 2015

All Your Sessions Are Belong to Us: Investigating Authenticator Leakage through Backup Channels on Android.

[BibT_eX]

[DOI]

Proceedings of the 20th International Conference on Engineering of Complex Computer Systems, 2015

Verifying Parameterized Timed Security Protocols.

[BibT_eX]

[DOI]

Proceedings of the FM 2015: Formal Methods, 2015

Heuristic Collective Learning for Efficient and Robust Emergence of Social Norms.

[BibT_eX]

[DOI]

Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, 2015

2014

Learning Assumptions for CompositionalVerification of Timed Systems.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2014

Towards Formal Modelling and Verification of Pervasive Computing Systems.

[BibT_eX]

[DOI]

Trans. Comput. Collect. Intell., 2014

Parameter synthesis for hierarchical concurrent real-time systems.

[BibT_eX]

[DOI]

Real Time Syst., 2014

Complexity of the Soundness Problem of Workflow Nets.

[BibT_eX]

[DOI]

Fundam. Informaticae, 2014

Model checking approach to automated planning.

[BibT_eX]

[DOI]

Formal Methods Syst. Des., 2014

Model checking with fairness assumptions using PAT.

[BibT_eX]

[DOI]

Frontiers Comput. Sci., 2014

Towards verification of computation orchestration.

[BibT_eX]

[DOI]

Formal Aspects Comput., 2014

Stateful Security Protocol Verification.

[BibT_eX]

[DOI]

CoRR, 2014

Automated runtime recovery for QoS-based service composition.

[BibT_eX]

[DOI]

Proceedings of the 23rd International World Wide Web Conference, 2014

Are Timed Automata Bad for a Specification Language? Language Inclusion Checking for Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2014

RaPiD: a toolkit for reliability analysis of non-deterministic systems.

[BibT_eX]

[DOI]

Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE-22), Hong Kong, China, November 16, 2014

Automatic early defects detection in use case documents.

[BibT_eX]

[DOI]

Proceedings of the ACM/IEEE International Conference on Automated Software Engineering, 2014

Event Analytics.

[BibT_eX]

[DOI]

Proceedings of the Theoretical Aspects of Computing - ICTAC 2014, 2014

Clonepedia: Summarizing Code Clones by Common Syntactic Context for Software Maintenance.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE International Conference on Software Maintenance and Evolution, Victoria, BC, Canada, September 29, 2014

Detecting differences across multiple instances of code clones.

[BibT_eX]

[DOI]

Proceedings of the 36th International Conference on Software Engineering, 2014

VeriWS: a tool for verification of combined functional and non-functional requirements of web service composition.

[BibT_eX]

[DOI]

Proceedings of the 36th International Conference on Software Engineering, 2014

GPU Accelerated Counterexample Generation in LTL Model Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2014

TAuth: Verifying Timed Security Protocols.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2014

Practical Analysis Framework for Software-Based Attestation Scheme.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2014

SCC-Based Improved Reachability Analysis for Markov Decision Processes.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2014

A Hybrid Model of Connectors in Cyber-Physical Systems.

[BibT_eX]

[DOI]

Xiaohong Chen

Sai Sathyanarayan Venkatraman

Meng Sun

Proceedings of the Formal Methods and Software Engineering, 2014

Symbolic Analysis of an Electric Vehicle Charging Protocol.

[BibT_eX]

[DOI]

Proceedings of the 2014 19th International Conference on Engineering of Complex Computer Systems, 2014

Adaptive Defending Strategy for Smart Grid Attacks.

[BibT_eX]

[DOI]

Proceedings of the 2nd Workshop on Smart Energy Grid Security, 2014

Diamonds Are a Girl's Best Friend: Partial Order Reduction for Timed Automata with Abstractions.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

Towards a Combination of CafeOBJ and PAT.

[BibT_eX]

[DOI]

Proceedings of the Specification, Algebra, and Software, 2014

An extensive model checking framework for multi-agent systems.

[BibT_eX]

[DOI]

Proceedings of the International conference on Autonomous Agents and Multi-Agent Systems, 2014

2013

Verifying Linearizability via Optimized Refinement Checking.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2013

Modeling and verifying hierarchical real-time systems using stateful timed CSP.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2013

State Space Reduction for Sensor Networks Using Two-Level Partial Order Reduction.

[BibT_eX]

[DOI]

Proceedings of the Verification, 2013

USMMC: a self-contained model checker for UML state machines.

[BibT_eX]

[DOI]

Proceedings of the Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2013

Towards Formal Modeling and Verification of Cloud Architectures: A Case Study on Hadoop.

[BibT_eX]

[DOI]

Rajaraman Kanagasabai

Proceedings of the IEEE Ninth World Congress on Services, 2013

Social-Loc: improving indoor localization with social sensing.

[BibT_eX]

[DOI]

Proceedings of the 11th ACM Conference on Embedded Network Sensor Systems, 2013

AUTHSCAN: Automatic Extraction of Web Authentication Protocols from Implementations.

[BibT_eX]

[DOI]

Guangdong Bai

Jike Lei

Guozhu Meng

Proceedings of the 20th Annual Network and Distributed System Security Symposium, 2013

Constraint-based automatic symmetry detection.

[BibT_eX]

[DOI]

Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

TzuYu: Learning stateful typestates.

[BibT_eX]

[DOI]

Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

Automatically partition software into least privilege components using dynamic data dependency analysis.

[BibT_eX]

[DOI]

Proceedings of the 2013 28th IEEE/ACM International Conference on Automated Software Engineering, 2013

Combining model checking and testing with an application to reliability prediction and distribution.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Software Testing and Analysis, 2013

Improved Reachability Analysis in DTMC via Divide and Conquer.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 10th International Conference, 2013

A Formal Semantics for Complete UML State Machines with Communications.

[BibT_eX]

[DOI]

Proceedings of the Integrated Formal Methods, 10th International Conference, 2013

Dynamic synthesis of local time requirement for service composition.

[BibT_eX]

[DOI]

Proceedings of the 35th International Conference on Software Engineering, 2013

Build your own model checker in one month.

[BibT_eX]

[DOI]

Proceedings of the 35th International Conference on Software Engineering, 2013

Improving Model Checking Stateful Timed CSP with non-Zenoness through Clock-Symmetry Reduction.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2013

A UTP Semantics for Communicating Processes with Shared Variables.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2013

vTRUST: A Formal Modeling and Verification Framework for Virtualization Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2013

Verification of Functional and Non-functional Requirements of Web Service Composition.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2013

TTM/PAT: Specifying and Verifying Timed Transition Models.

[BibT_eX]

[DOI]

Proceedings of the Formal Techniques for Safety-Critical Systems, 2013

PSyHCoS: Parameter Synthesis for Hierarchical Concurrent Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 25th International Conference, 2013

CELL: A Compositional Verification Framework.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2013

Multi-core Model Checking Algorithms for LTL Verification with Fairness Assumptions.

[BibT_eX]

[DOI]

Proceedings of the 20th Asia-Pacific Software Engineering Conference, 2013

2012

Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Finite State Based Models and Applications., 2012

Formal modeling and validation of Stateflow diagrams.

[BibT_eX]

[DOI]

Int. J. Softw. Tools Technol. Transf., 2012

SeVe: automatic tool for verification of security protocols.

[BibT_eX]

[DOI]

Frontiers Comput. Sci. China, 2012

Planning as Model Checking Tasks.

[BibT_eX]

[DOI]

Proceedings of the 35th Annual IEEE Software Engineering Workshop, 2012

Improving indoor localization with social interactions.

[BibT_eX]

[DOI]

Proceedings of the 10th ACM Conference on Embedded Network Sensor Systems, 2012

Probabilistic Model Checking Multi-agent Behaviors in Dispersion Games Using Counter Abstraction.

[BibT_eX]

[DOI]

Proceedings of the PRIMA 2012: Principles and Practice of Multi-Agent Systems, 2012

Analyzing multi-agent systems with probabilistic model checking approach.

[BibT_eX]

[DOI]

Proceedings of the 34th International Conference on Software Engineering, 2012

More Anti-chain Based Refinement Checking.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2012

An Analytical and Experimental Comparison of CSP Extensions and Tools.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2012

Symbolic Model-Checking of Stateful Timed CSP Using BDD and Digitization.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2012

Automatic Generation of Provably Correct Embedded Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2012

Formal Analysis of Pervasive Computing Systems.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, 2012

Translating PDDL into CSP# - The PAT Approach.

[BibT_eX]

[DOI]

Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, 2012

Model Checking Software Architecture Design.

[BibT_eX]

[DOI]

Proceedings of the 14th International IEEE Symposium on High-Assurance Systems Engineering, 2012

Improved BDD-Based Discrete Analysis of Timed Systems.

[BibT_eX]

[DOI]

Proceedings of the FM 2012: Formal Methods, 2012

Automatic Compositional Verification of Timed Systems.

[BibT_eX]

[DOI]

Proceedings of the FM 2012: Formal Methods, 2012

A Model Checker for Hierarchical Probabilistic Real-Time Systems.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 24th International Conference, 2012

Using Monterey Phoenix to Formalize and Verify System Architectures.

[BibT_eX]

[DOI]

Proceedings of the 19th Asia-Pacific Software Engineering Conference, 2012

Complexity of the Soundness Problem of Bounded Workflow Nets.

[BibT_eX]

[DOI]

Proceedings of the Application and Theory of Petri Nets - 33rd International Conference, 2012

2011

Towards bug-free implementation for wireless sensor networks.

[BibT_eX]

[DOI]

Proceedings of the 9th International Conference on Embedded Networked Sensor Systems, 2011

A model checking framework for hierarchical systems.

[BibT_eX]

[DOI]

Proceedings of the 26th IEEE/ACM International Conference on Automated Software Engineering (ASE 2011), 2011

PAT 3: An Extensible Architecture for Building Multi-domain Model Checkers.

[BibT_eX]

[DOI]

Proceedings of the IEEE 22nd International Symposium on Software Reliability Engineering, 2011

Towards a Model Checker for NesC and Wireless Sensor Networks.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2011

Differencing Labeled Transition Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2011

Verification of Orchestration Systems Using Compositional Partial Order Reduction.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2011

PRTS: An Approach for Model Checking Probabilistic Real-Time Hierarchical Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2011

On Combining State Space Reductions with Global Fairness Assumptions.

[BibT_eX]

[DOI]

Proceedings of the FM 2011: Formal Methods, 2011

An Efficient Algorithm for Learning Event-Recording Automata.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2011

2010

A verification system for interval-based specification languages.

[BibT_eX]

[DOI]

ACM Trans. Softw. Eng. Methodol., 2010

Analyzing hierarchical complex real-time systems.

[BibT_eX]

[DOI]

Proceedings of the 18th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2010

SpecDiff: debugging formal specifications.

[BibT_eX]

[DOI]

Proceedings of the ASE 2010, 2010

Model Checking Hierarchical Probabilistic Systems.

[BibT_eX]

[DOI]

Songzheng Song

Proceedings of the Formal Methods and Software Engineering, 2010

Model Checking a Model Checker: A Code Contract Combined Approach.

[BibT_eX]

[DOI]

Bin Cheng

Proceedings of the Formal Methods and Software Engineering, 2010

Developing Model Checkers Using PAT.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2010

Model-Based Methods for Linking Web Service Choreography and Orchestration.

[BibT_eX]

[DOI]

Proceedings of the 17th Asia Pacific Software Engineering Conference, 2010

2009

A formal framework for modeling and validating Simulink diagrams.

[BibT_eX]

[DOI]

Chunqing Chen

Formal Aspects Comput., 2009

Integrating Specification and Programs for System Modeling and Verification.

[BibT_eX]

[DOI]

Proceedings of the TASE 2009, 2009

Verification of Population Ring Protocols in PAT.

[BibT_eX]

[DOI]

Proceedings of the TASE 2009, 2009

Towards Expressive Specification and Efficient Model Checking.

[BibT_eX]

[DOI]

Proceedings of the TASE 2009, 2009

Formal Verification of Scalable NonZero Indicators.

[BibT_eX]

Proceedings of the 21st International Conference on Software Engineering & Knowledge Engineering (SEKE'2009), 2009

Verifying Stateful Timed CSP Using Implicit Clocks and Zone Abstraction.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2009

Scalable Multi-core Model Checking Fairness Enhanced Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2009

Fair Model Checking with Process Counter Abstraction.

[BibT_eX]

[DOI]

Proceedings of the FM 2009: Formal Methods, 2009

Model Checking Linearizability via Refinement.

[BibT_eX]

[DOI]

Proceedings of the FM 2009: Formal Methods, 2009

PAT: Towards Flexible Verification under Fairness.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 21st International Conference, 2009

2008

Timed Automata Patterns.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2008

Compositional encoding for bounded model checking.

[BibT_eX]

[DOI]

Frontiers Comput. Sci. China, 2008

Bounded Model Checking of Compositional Processes.

[BibT_eX]

[DOI]

Proceedings of the Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, 2008

Model Checking CSP Revisited: Introducing a Process Analysis Toolkit.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, 2008

An analyzer for extended compositional process algebras.

[BibT_eX]

[DOI]

Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), 2008

A verification system for timed interval calculus.

[BibT_eX]

[DOI]

Chunqing Chen

Proceedings of the 30th International Conference on Software Engineering (ICSE 2008), 2008

Specifying and Verifying Event-Based Fairness Enhanced Systems.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2008

Specifying and Verifying Sensor Networks: An Experiment of Formal Methods.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2008

A Scalable Approach to Multi-style Architectural Modeling and Verification.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Engineering of Complex Computer Systems (ICECCS 2008), March 31 2008, 2008

A Formal Model of Semantic Web Service Ontology (WSMO) Execution.

[BibT_eX]

[DOI]

Proceedings of the 13th International Conference on Engineering of Complex Computer Systems (ICECCS 2008), March 31 2008, 2008

2007

Realizing Live Sequence Charts in SystemVerilog.

[BibT_eX]

[DOI]

Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

Machine-Assisted Proof Support for Validation Beyond Simulink.

[BibT_eX]

[DOI]

Chunqing Chen

Proceedings of the Formal Methods and Software Engineering, 2007

A Formal Semantic Model of the Semantic Web Service Ontology (WSMO).

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007

2006

Design Synthesis from Interaction and State-Based Specifications.

[BibT_eX]

[DOI]

IEEE Trans. Software Eng., 2006

Reasoning support for Semantic Web ontology family languages using Alloy.

[BibT_eX]

[DOI]

Multiagent Grid Syst., 2006

Reasoning About ORA-SS Data Models Using the Semantic Web.

[BibT_eX]

[DOI]

J. Data Semant., 2006

Validating Semistructured Data Using OWL.

[BibT_eX]

[DOI]

Proceedings of the Advances in Web-Age Information Management, 2006

Context Awareness Systems Design and Reasoning.

[BibT_eX]

[DOI]

Proceedings of the Leveraging Applications of Formal Methods, 2006

Verification of Computation Orchestration Via Timed Automata.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2006

A Reasoning Method for Timed CSP Based on Constraint Solving.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2006

2005

Algorithmic Design Using Object-Z for Twig XML Queries Evaluation.

[BibT_eX]

[DOI]

Proceedings of the International Workshop on Web Languages and Formal Methods, 2005

Visualizing and Simulating Semantic Web Services Ontologies.

[BibT_eX]

[DOI]

Proceedings of the Formal Methods and Software Engineering, 2005

Model Checking Live Sequence Charts.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Engineering of Complex Computer Systems (ICECCS 2005), 2005

Extracting FSMs from Object-Z Specifications with History Invariants.

[BibT_eX]

[DOI]

Proceedings of the 10th International Conference on Engineering of Complex Computer Systems (ICECCS 2005), 2005

Synthesis of Distributed Processes from Scenario-Based Specifications.

[BibT_eX]

[DOI]

Proceedings of the FM 2005: Formal Methods, 2005

A Tools Environment for Developing and Reasoning about Ontologies.

[BibT_eX]

[DOI]

Proceedings of the 12th Asia-Pacific Software Engineering Conference (APSEC 2005), 2005

2004

Generating MSCs from an Integrated Formal Specification Language.

[BibT_eX]

[DOI]

Shengchao Qin