Jifeng He
According to our database^{1},
Jifeng He
authored at least 195 papers
between 1983 and 2020.
Collaborative distances:
Collaborative distances:
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at wikidata.org

at viaf.org

at id.loc.gov

at dnb.info
On csauthors.net:
Bibliography
2020
Statistical Model CheckingBased Evaluation and Optimization for Cloud Workflow Resource Allocation.
IEEE Trans. Cloud Comput., 2020
2019
Toward a Unified Executable Formal Automobile OS Kernel and Its Applications.
IEEE Trans. Reliability, 2019
Theoretical and Practical Aspects of Linking Operational and Algebraic Semantics for MDESL.
ACM Trans. Softw. Eng. Methodol., 2019
AADL+: a simulationbased methodology for cyberphysical systems.
Frontiers Comput. Sci., 2019
Robustness Verification of Classification Deep Neural Networks via Linear Programming.
Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, 2019
2018
A new roadmap for linking theories of programming and its applications on GCL and CSP.
Sci. Comput. Program., 2018
Accelerating LTL satisfiability checking by SAT solvers.
J. Log. Comput., 2018
An explicit transition system construction approach to LTL satisfiability checking.
Formal Asp. Comput., 2018
Linking Theories of Probabilistic Programming.
Proceedings of the Symposium on RealTime and Hybrid Systems, 2018
2017
A Survey on DataFlow Testing.
ACM Comput. Surv., 2017
A Hybrid Relational Modelling Language.
Proceedings of the Concurrency, Security, and Puzzles, 2017
2016
SMTBased Symbolic Encoding and Formal Analysis of HML Models.
MONET, 2016
Fusing Incomplete Multisensor Heterogeneous Data to Estimate Urban Traffic.
IEEE Multim., 2016
Automated coveragedriven testing: combining symbolic execution and model checking.
Sci. China Inf. Sci., 2016
A New Roadmap for Linking Theories of Programming.
Proceedings of the Unifying Theories of Programming  6th International Symposium, 2016
2015
Modeling and analysis of interactive telemedicine systems.
ISSE, 2015
Semantic theories of programs with nested interrupts.
Frontiers Comput. Sci., 2015
Denotational semantics and its algebraic derivation for an eventdriven systemlevel language.
Formal Asp. Comput., 2015
Combining Symbolic Execution and Model Checking for Data Flow Testing.
Proceedings of the 37th IEEE/ACM International Conference on Software Engineering, 2015
Probabilistic Denotational Semantics for an Interrupt Modelling Language.
Proceedings of the 20th International Conference on Engineering of Complex Computer Systems, 2015
2014
Investigating System Survivability from a Probabilistic Perspective.
IEICE Trans. Inf. Syst., 2014
A UTP semantic model for Orc language with execution status and fault handling.
Frontiers Comput. Sci., 2014
Fast LTL Satisfiability Checking by SAT Solvers.
CoRR, 2014
A Formal Model for a Hybrid Programming Language.
Proceedings of the Unifying Theories of Programming  5th International Symposium, 2014
Automated CoverageDriven Test Data Generation Using Dynamic Symbolic Execution.
Proceedings of the Eighth International Conference on Software Security and Reliability, 2014
Aalta: an LTL satisfiability checker over Infinite/Finite traces.
Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, (FSE22), Hong Kong, China, November 16, 2014
LTLf Satisfiability Checking.
Proceedings of the ECAI 2014  21st European Conference on Artificial Intelligence, 1822 August 2014, Prague, Czech Republic, 2014
2013
A novel requirement analysis approach for periodic control systems.
Frontiers Comput. Sci., 2013
Hybrid MARTE statecharts.
Frontiers Comput. Sci., 2013
Polsat: A Portfolio LTL Satisfiability Solver.
CoRR, 2013
LTL Satisfiability Checking Revisited.
Proceedings of the 2013 20th International Symposium on Temporal Representation and Reasoning, 2013
A ClockBased Framework for Construction of Hybrid Systems.
Proceedings of the Theoretical Aspects of Computing  ICTAC 2013, 2013
Deadline Analysis of AUTOSAR OS Periodic Tasks in the Presence of Interrupts.
Proceedings of the Formal Methods and Software Engineering, 2013
Hybrid Relation Calculus.
Proceedings of the 2013 18th International Conference on Engineering of Complex Computer Systems, 2013
Boundoriented parallel pruning approaches for efficient resource constrained scheduling of highlevel synthesis.
Proceedings of the International Conference on Hardware/Software Codesign and System Synthesis, 2013
On the Relationship between LTL Normal Forms and Büchi Automata.
Proceedings of the Theories of Programming and Formal Methods, 2013
2012
Linking operational semantics and algebraic semantics for a probabilistic timed sharedvariable language.
J. Log. Algebraic Methods Program., 2012
MDM: A Mode Diagram Modeling Framework
Proceedings of the Proceedings First International Workshop on Formal Techniques for SafetyCritical Systems, 2012
On the Relationship between LTL Normal Forms and Buechi Automata
CoRR, 2012
MDM: A Mode Diagram Modeling Framework for Periodic Control Systems
CoRR, 2012
The stochastic semantics and verification for periodic control systems.
Sci. China Inf. Sci., 2012
Denotational Semantics for a Probabilistic Timed SharedVariable Language.
Proceedings of the Unifying Theories of Programming, 4th International Symposium, 2012
Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude.
Proceedings of the Unifying Theories of Programming, 4th International Symposium, 2012
Formal Specification of Hybrid MARTE Statecharts.
Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012
A Denotational Model for Instantaneous Signal Calculus.
Proceedings of the Software Engineering and Formal Methods  10th International Conference, 2012
ORIENTAIS: Formal Verified OSEK/VDX RealTime Operating System.
Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, 2012
Spatiotemporal UML Statechart for CyberPhysical Systems.
Proceedings of the 17th IEEE International Conference on Engineering of Complex Computer Systems, 2012
2011
Algebraic approach to linking the semantics of web services.
ISSE, 2011
MDA Approach for Nonfunctional Properties of Dependable and Distributed RealTime Systems.
Proceedings of the Convergence and Hybrid Information Technology, 2011
AspectOriented QoS Specification for CyberPhysical Systems.
Proceedings of the Convergence and Hybrid Information Technology, 2011
A Formal Framework for AspectOriented Specification of Cyber Physical Systems.
Proceedings of the Convergence and Hybrid Information Technology, 2011
Towards a Signal Calculus for EventBased Synchronous Languages.
Proceedings of the Formal Methods and Software Engineering, 2011
Formal Model of Interrupt Program from a Probabilistic Perspective.
Proceedings of the 16th IEEE International Conference on Engineering of Complex Computer Systems, 2011
A Unifying Approach to Validating SpecificationOriented XML Constraints.
Proceedings of the 13th IEEE International Symposium on HighAssurance Systems Engineering, 2011
2010
CSP is a retract of CCS.
Theor. Comput. Sci., 2010
Linking denotational semantics with operational semantics for web services.
ISSE, 2010
A process algebraic framework for specification and validation of realtime systems.
Formal Asp. Comput., 2010
Generating Denotational Semantics from Algebraic Semantics for EventDriven SystemLevel Language.
Proceedings of the Unifying Theories of Programming  Third International Symposium, 2010
A Probabilistic BPELLike Language.
Proceedings of the Unifying Theories of Programming  Third International Symposium, 2010
SPARDL: A Requirement Modeling Language for Periodic Control System.
Proceedings of the Leveraging Applications of Formal Methods, Verification, and Validation, 2010
A Denotational Semantical Model for Orc Language.
Proceedings of the Theoretical Aspects of Computing, 2010
Probabilistic Programming with Coordination.
Proceedings of the Reflections on the Work of C. A. R. Hoare., 2010
2009
PTSC: probability, time and sharedvariable concurrency.
ISSE, 2009
Mutation testing in UTP.
Formal Asp. Comput., 2009
Probabilistic Programming With Coordination and Compensation.
Proceedings of the Third IEEE International Conference on Secure Software Integration and Reliability Improvement, 2009
Animating the Link Between Operational Semantics and Algebraic Semantics for a Probabilistic Timed SharedVariable Language.
Proceedings of the 33rd Annual IEEE Software Engineering Workshop, 2009
LocalityBased Normal Form Approach to Linking Algebraic Semantics and Operational Semantics for an EventDriven SystemLevel Language.
Proceedings of the 20th Australian Software Engineering Conference (ASWEC 2009), 2009
A Formal Perspective for Service Coordination Framework in Service Oriented Architecture.
Proceedings of the 20th Australian Software Engineering Conference (ASWEC 2009), 2009
2008
From algebraic semantics to denotational semantics for Verilog.
ISSE, 2008
Service refinement.
Sci. China Ser. F Inf. Sci., 2008
Denotational Approach to an EventDriven SystemLevel Language.
Proceedings of the Unifying Theories of Programming, Second International Symposium, 2008
Transaction Calculus  (Invited Paper).
Proceedings of the Unifying Theories of Programming, Second International Symposium, 2008
Modelling Coordination and Compensation.
Proceedings of the Leveraging Applications of Formal Methods, 2008
An Observational Model for Transactional Calculus of Services Orchestration.
Proceedings of the Theoretical Aspects of Computing, 2008
Refinement and test case generation in Unifying Theory of Programming.
Proceedings of the 24th IEEE International Conference on Software Maintenance (ICSM 2008), September 28, 2008
A Denotational Model for Web Services Choreography.
Proceedings of the Distributed Computing and Internet Technology, 2008
Towards the Service Composition Through Buses.
Proceedings of the 11th IEEE High Assurance Systems Engineering Symposium, 2008
Transaction Calculus.
Proceedings of the 11th IEEE High Assurance Systems Engineering Symposium, 2008
Specifying and Verifying Web Transactions.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2008
Execution Semantics for rCOS.
Proceedings of the 15th AsiaPacific Software Engineering Conference (APSEC 2008), 2008
2007
A model for BPELlike languages.
Frontiers Comput. Sci. China, 2007
Refinement and Test Case Generation in UTP.
Electron. Notes Theor. Comput. Sci., 2007
Scalable Formalization of Publish/Subscribe Messaging Scheme Based on Message Brokers.
Proceedings of the Web Services and Formal Methods, 4th International Workshop, 2007
An Operational Approach to BPELlike Programming.
Proceedings of the 31st Annual IEEE / NASA Software Engineering Workshop (SEW31 2007), 2007
Algebraic Approach to Operational Semantics and ObservationOriented Semantics for a Timed SharedVariable Language with Probability.
Proceedings of the 31st Annual IEEE / NASA Software Engineering Workshop (SEW31 2007), 2007
Looking into Compensable Transactions.
Proceedings of the 31st Annual IEEE / NASA Software Engineering Workshop (SEW31 2007), 2007
An Inconsistency Free Formalization of B/S Architecture.
Proceedings of the 31st Annual IEEE / NASA Software Engineering Workshop (SEW31 2007), 2007
Modeling and Verifying Web Services Choreography Using Process Algebra.
Proceedings of the 31st Annual IEEE / NASA Software Engineering Workshop (SEW31 2007), 2007
UTP Semantics for Web Services.
Proceedings of the Integrated Formal Methods, 6th International Conference, 2007
Algebraic Semantics for Compensable Transactions.
Proceedings of the Theoretical Aspects of Computing, 2007
Linking Semantic Models.
Proceedings of the Theoretical Aspects of Computing, 2007
A Formal Model for Compensable Transactions.
Proceedings of the 12th International Conference on Engineering of Complex Computer Systems (ICECCS 2007), 2007
Unifying Denotational Semantics with Operational Semantics for Web Services.
Proceedings of the Distributed Computing and Internet Technology, 2007
A Model of ComponentBased Programming.
Proceedings of the International Symposium on Fundamentals of Software Engineering, 2007
Compensable Programs.
Proceedings of the Formal Methods and Hybrid RealTime Systems, 2007
The Validation and Verification of WSCDL.
Proceedings of the 14th AsiaPacific Software Engineering Conference (APSEC 2007), 2007
2006
rCOS: A refinement calculus of object systems.
Theor. Comput. Sci., 2006
From Statecharts to Verilog: a formal approach to hardware/software cospecification.
ISSE, 2006
A Theory of Reactive Components.
Electron. Notes Theor. Comput. Sci., 2006
A strategy for service realization in serviceoriented design.
Sci. China Ser. F Inf. Sci., 2006
Unifying Probability.
Proceedings of the Unifying Theories of Programming, First International Symposium, 2006
Constructing PropertyOriented Models for Verification.
Proceedings of the Unifying Theories of Programming, First International Symposium, 2006
Integrating Probability with Time and SharedVariable Concurrency.
Proceedings of the 30th Annual IEEE / NASA Software Engineering Workshop (SEW30 2006), 2006
An Operational Semantics of an EventDriven SystemLevel Simulator.
Proceedings of the 30th Annual IEEE / NASA Software Engineering Workshop (SEW30 2006), 2006
A Hybrid Heuristic Algorithm for HWSW Partitioning Within Timed Automata.
Proceedings of the KnowledgeBased Intelligent Information and Engineering Systems, 2006
Patterns with Algebraic Properties in BPEL0.
Proceedings of the Leveraging Applications of Formal Methods, 2006
Towards the Semantics for Web Service Choreography Description Language.
Proceedings of the Formal Methods and Software Engineering, 2006
Integrating Timed Automata into Tabu Algorithm for HWSW Partitioning.
Proceedings of the 11th International Conference on Engineering of Complex Computer Systems (ICECCS 2006), 2006
Reactive Component based ServiceOriented Design  A Case Study.
Proceedings of the 11th International Conference on Engineering of Complex Computer Systems (ICECCS 2006), 2006
Theoretical Foundations of ScopeBased Compensable Flow Language for Web Service.
Proceedings of the Formal Methods for Open ObjectBased Distributed Systems, 2006
An Optimal LowerBound Algorithm for the HighLevel Synthesis Scheduling Problem.
Proceedings of the 9th IEEE Workshop on Design & Diagnostics of Electronic Circuits & Systems (DDECS 2006), 2006
A Denotational Approach to ScopeBased Compensable Flow Language for Web Service.
Proceedings of the Advances in Computer Science, 2006
2005
Exploring optimal solution to hardware/software partitioning for synchronous model.
Formal Asp. Comput., 2005
Integrating Time and Resource into Circus.
Electron. Notes Theor. Comput. Sci., 2005
Towards a Rigorous Approach to UMLBased Development.
Electron. Notes Theor. Comput. Sci., 2005
Integrating Theories and Techniques for Program Modelling, Design and Verification.
Proceedings of the Verified Software: Theories, 2005
Towards A Truly Concurrent Model for Processes Sharing Resources.
Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005), 2005
POST: A Case Study for an Incremental Development in rCOS.
Proceedings of the Theoretical Aspects of Computing, 2005
ComponentBased Software Engineering.
Proceedings of the Theoretical Aspects of Computing, 2005
Linking Theories of Concurrency.
Proceedings of the Theoretical Aspects of Computing, 2005
Consistency Checking of UML Requirements.
Proceedings of the 10th International Conference on Engineering of Complex Computer Systems (ICECCS 2005), 2005
Linking Theories of Concurrency by Retraction.
Proceedings of the Distributed Computing and Internet Technology, 2005
Consistent Code Generation from UML Models.
Proceedings of the 16th Australian Software Engineering Conference (ASWEC 2005), 31 March, 2005
2004
Unifying Views of UML.
Electron. Notes Theor. Comput. Sci., 2004
Resource Models and PreCompiler Specification for Hardware/Software CoDesign Language.
Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004
An Approach to Hardware/Software Partitioning for Multiple Hardware Devices Model.
Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), 2004
An Optimal Approach to Hardware/Software Partitioning for Synchronous Model.
Proceedings of the Integrated Formal Methods, 4th International Conference, 2004
Contract Oriented Development of Component Software.
Proceedings of the Exploring New Frontiers of Theoretical Informatics, 2004
A Framework for Specification and Validation of RealTime Systems Using Circus Actions.
Proceedings of the Theoretical Aspects of Computing, 2004
Integrating Variants of DC.
Proceedings of the Theoretical Aspects of Computing, 2004
Deriving Probabilistic Semantics Via the 'Weakest Completion'.
Proceedings of the Formal Methods and Software Engineering, 2004
Generating a Prototype from a UML Model of System Requirements.
Proceedings of the Distributed Computing and Internet Technology, 2004
rCOS: Refinement of Component and Object Systems.
Proceedings of the Formal Methods for Components and Objects, 2004
Linking Theories of Concurrency.
Proceedings of the Communicating Sequential Processes: The First 25 Years, 2004
Linking UML Models of Design and Requirement.
Proceedings of the 15th Australian Software Engineering Conference (ASWEC 2004), 2004
A Formal Semantics of UML Sequence Diagram.
Proceedings of the 15th Australian Software Engineering Conference (ASWEC 2004), 2004
A Relational Model for ObjectOriented Designs.
Proceedings of the Programming Languages and Systems: Second Asian Symposium, 2004
2003
Advanced Features of Duration Calculus and Their Applications in Sequential Hybrid Programs.
Formal Asp. Comput., 2003
Towards a Theory of Bisimulation for a Fragment of Verilog.
Proceedings of the 17th International Parallel and Distributed Processing Symposium (IPDPS 2003), 2003
A Relational Model for Formal ObjectOriented Requirement Analysis in UML.
Proceedings of the Formal Methods and Software Engineering, 2003
2002
An Algebraic Hardware/Software Partitioning Algorithm.
J. Comput. Sci. Technol., 2002
An Algebraic Approach to the VERILOG Programming.
Proceedings of the Formal Methods at the Crossroads. From Panacea to Foundational Support, 2002
Towards a Time Model for Circus.
Proceedings of the Formal Methods and Software Engineering, 2002
Hardware/Software Partitioning in Verilog.
Proceedings of the Formal Methods and Software Engineering, 2002
Using Transition Systems to Unify UML Models.
Proceedings of the Formal Methods and Software Engineering, 2002
Soundness, Completeness and Nonredundancy of Operational Semantics for Verilog Based on Denotational Semantics.
Proceedings of the Formal Methods and Software Engineering, 2002
Integrating CSP and DC.
Proceedings of the 8th International Conference on Engineering of Complex Computer Systems (ICECCS 2002), 2002
Towards a Refinement Calculus for Object Systems.
Proceedings of the 1st IEEE International Conference on Cognitive Informatics (ICCI 2002), 2002
2001
An Approach to the Specification and Verification of a Hardware Compilation Scheme.
J. Supercomput., 2001
Formal and UseCase Driven Requirement Analysis in UML.
Proceedings of the 25th International Computer Software and Applications Conference (COMPSAC 2001), 2001
From Operational Semantics to Denotational Semantics for Verilog.
Proceedings of the Correct Hardware Design and Verification Methods, 2001
Deriving Operational Semantics from Denotational Semantics for Verilog.
Proceedings of the 8th AsiaPacific Software Engineering Conference (APSEC 2001), 2001
A Theory of Combinational Programs.
Proceedings of the 8th AsiaPacific Software Engineering Conference (APSEC 2001), 2001
Partitioning Program into Hardware and Software.
Proceedings of the 8th AsiaPacific Software Engineering Conference (APSEC 2001), 2001
Constructing Hardware/Software Interface Using Protocol Converters.
Proceedings of the 2nd AsiaPacific Conference on Quality Software (APAQS 2001), 2001
2000
An Operational Semantics of a Simulator Algorithm.
Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 2000
An Animatable Operational Semantics of the Verilog Hardware Description Language.
Proceedings of the 3rd IEEE International Conference on Formal Engineering Methods, 2000
Algebraic derivation of an operational semantics.
Proceedings of the Proof, Language, and Interaction, Essays in Honour of Robin Milner, 2000
Unifying theories of healthiness condition.
Proceedings of the 7th AsiaPacific Software Engineering Conference (APSEC 2000), 2000
1999
Linking Theories in Probabilistic Programming.
Inf. Sci., 1999
A Denotational Semantics of Timed RSL Using Duration Calculus.
Proceedings of the 6th International Workshop on RealTime Computing and Applications Symposium (RTCSA '99), 1999
A Common Framework for Mixed Hardware/Software Systems.
Proceedings of the Integrated Formal Methods, 1999
A Behavioral Model for Codesign.
Proceedings of the FM'99  Formal Methods, 1999
A Trace Model for Pointers and Objects.
Proceedings of the ECOOP'99, 1999
1998
Unifying theories of programming.
Proceedings of the Participants Copies for Relational Methods in Logic, 1998
1997
Probabilistic Models for the Guarded Command Language.
Sci. Comput. Program., 1997
The RelyGuarantee Method for Verifying Shared Variable Concurrent Programs.
Formal Asp. Comput., 1997
Unifying Theories for Parallel Programming.
Proceedings of the EuroPar '97 Parallel Processing, 1997
Linking Theories in Probabilistic Programming.
Proceedings of the Participants Copies of Third International Seminar on the Use of Relational Methods in Computer Science, 1997
1996
Algebraic Laws for BSP Programming.
Proceedings of the EuroPar '96 Parallel Processing, 1996
1994
A SpecificationOriented Semantics for the Refinement of RealTime Systems.
Theor. Comput. Sci., 1994
Specification, Verification and Prototyping of an Optimized Compiler.
Formal Asp. Comput., 1994
Laws of Parallel Programming with Shared Variables.
Proceedings of the 6th Refinement Workshop, 1994
Simulation Approach to Provably Correct Hardware Compilation.
Proceedings of the Formal Techniques in RealTime and FaultTolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994
Provably Correct Systems.
Proceedings of the Formal Techniques in RealTime and FaultTolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994
1993
From Algebra to Operational Semantics.
Inf. Process. Lett., 1993
Normal Form Approach to Compiler Design.
Acta Informatica, 1993
A Predicative Semantics for the Refinement of RealTime Systems.
Proceedings of the Mathematical Foundations of Programming Semantics, 1993
RealTime Refinement: Semantics and Application.
Proceedings of the Mathematical Foundations of Computer Science 1993, 1993
Hybrid Parallel Programming and Implementation of Synchronised Communication.
Proceedings of the Mathematical Foundations of Computer Science 1993, 1993
Towards a Provably Correct Hardware Implementation of Occam.
Proceedings of the Correct Hardware Design and Verification Methods, 1993
1992
A case study in formally developing statebased parallel programs  the Dutch National Torus.
Proceedings of the 5th Refinement Workshop, 1992
Time interval semantics and implementation of a realtime programming language.
Proceedings of the Fourth Euromicro workshop on RealTime Systems, 1992
1991
PreAdjunctions in Order Enriched Categories.
Math. Struct. Comput. Sci., 1991
1990
An Approach to Verifiable Compiling Specification and Prototyping.
Proceedings of the Programming Language Implementation and Logic Programming, 1990
A Theory of Synchrony and Asynchrony.
Proceedings of the Programming concepts and methods: Proceedings of the IFIP Working Group 2.2, 1990
1989
Process Simulation and Refinement.
Formal Asp. Comput., 1989
Various Simulations and Refinements.
Proceedings of the Stepwise Refinement of Distributed Systems, 1989
Categorical Semantics for Programming Languages.
Proceedings of the Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29, 1989
1987
Prespecification in Data Refinement.
Inf. Process. Lett., 1987
The Weakest Prespecification.
Inf. Process. Lett., 1987
Algebraic Specification and Proof of a Distributed Recovery Algorithm.
Distributed Comput., 1987
Laws of Programming.
Commun. ACM, 1987
1986
Data Refinement Refined.
Proceedings of the ESOP 86, 1986
1983
General Predicate Transformer and the Semantics of a Programming Language With Go To Statement.
Acta Informatica, 1983