Open Access. Powered by Scholars. Published by Universities.®
Programming Languages and Compilers Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Software Engineering (184)
- Databases and Information Systems (97)
- Artificial Intelligence and Robotics (57)
- Education (11)
- Graphics and Human Computer Interfaces (10)
-
- Theory and Algorithms (9)
- Computer Engineering (7)
- Engineering (7)
- Information Security (6)
- OS and Networks (5)
- Higher Education (4)
- Educational Methods (3)
- Numerical Analysis and Scientific Computing (3)
- Asian Studies (2)
- Computer and Systems Architecture (2)
- Data Storage Systems (2)
- Educational Assessment, Evaluation, and Research (2)
- Instructional Media Design (2)
- International and Area Studies (2)
- Social and Behavioral Sciences (2)
- Business (1)
- Curriculum and Instruction (1)
- Technology and Innovation (1)
- Keyword
-
- Model Check (22)
- Programming (13)
- Linear Temporal Logic (10)
- Label Transition System (8)
- Large Language Models (8)
-
- Large language models (8)
- Empirical study (7)
- Large Language Model (6)
- Operational Semantic (6)
- Code search (5)
- Large language model (5)
- Model Check Algorithm (5)
- Software engineering (5)
- Java (4)
- Model checking (4)
- Software testing (4)
- Stack Overflow (4)
- Strongly Connect Component (4)
- Formal Verification (3)
- Machine learning (3)
- Markov Decision Process (3)
- Martingales (3)
- Reinforcement learning (3)
- Simulated annealing (3)
- Software Engineering (3)
- Static Analysis (3)
- Symbolic Model Check (3)
- Verification (3)
- Active learning (2)
- Alignment (2)
Articles 241 - 270 of 379
Full-Text Articles in Programming Languages and Compilers
Clustering Classes In Packages For Program Comprehension, Xiaobing Sun, Xiangyue Liu, Bin Li, Bixin Li, David Lo, Lingzhi Liao
Clustering Classes In Packages For Program Comprehension, Xiaobing Sun, Xiangyue Liu, Bin Li, Bixin Li, David Lo, Lingzhi Liao
Research Collection School Of Computing and Information Systems
During software maintenance and evolution, one of the important tasks faced by developers is to understand a system quickly and accurately. With the increasing size and complexity of an evolving system, program comprehension becomes an increasingly difficult activity. Given a target system for comprehension, developers may first focus on the package comprehension. The packages in the system are of different sizes. For small-sized packages in the system, developers can easily comprehend them. However, for large-sized packages, they are difficult to understand. In this article, we focus on understanding these large-sized packages and propose a novel program comprehension approach for large-sized …
A Dynamic Programming Approach For Quickly Estimating Large Network-Based Mev Models, Tien Mai, Emma Frejinger, Mogens Fosgereau, Fabian Bastin
A Dynamic Programming Approach For Quickly Estimating Large Network-Based Mev Models, Tien Mai, Emma Frejinger, Mogens Fosgereau, Fabian Bastin
Research Collection School Of Computing and Information Systems
We propose a way to estimate a family of static Multivariate Extreme Value (MEV) models with large choice sets in short computational time. The resulting model is also straightforward and fast to use for prediction. Following Daly and Bierlaire (2006), the correlation structure is defined by a rooted, directed graph where each node without successor is an alternative. We formulate a family of MEV models as dynamic discrete choice models on graphs of correlation structures and show that the dynamic models are consistent with MEV theory and generalize the network MEV model (Daly and Bierlaire, 2006). Moreover, we show that …
Stochastic Invariants For Probabilistic Termination, Krishnendu Chatterjee, Petr Novotný, Dorde Zikelic
Stochastic Invariants For Probabilistic Termination, Krishnendu Chatterjee, Petr Novotný, Dorde Zikelic
Research Collection School Of Computing and Information Systems
Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability 1 (almost-sure termination). A powerful approach for this qualitative problem is the notion of ranking supermartingales with respect to a given set of invariants. The quantitative problem (probabilistic termination) asks for bounds on the termination probability, and this problem has not been addressed yet. A fundamental and conceptual drawback of the existing approaches to address probabilistic termination is that even though the supermartingales consider …
Towards Using Concurrent Java Api Correctly, Shuang Liu, Guangdong Bai, Jun Sun, Jin Song Dong
Towards Using Concurrent Java Api Correctly, Shuang Liu, Guangdong Bai, Jun Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Concurrent Programs are hard to analyze or debug due to the complex program logic and unpredictable execution environment. In practice, ordinary programmers often adopt existing well-designed concurrency related API (e.g., those in java.util.concurrent) so as to avoid dealing with these issues. These API can however often be used incorrectly, which results in hardto-debug concurrent bugs. In this work, we propose an approach for enforcing the correct usage of concurrency-related Java API. Our idea is to annotate concurrency-related Java classes with annotations related to misuse of these API and develop lightweight type checker to detect concurrent API misuse based on the …
Designing And Evaluating Business Process Models: An Experimental Approach, Yuecheng Martin Yu, Alexander Pelaez, Karl R. Lang
Designing And Evaluating Business Process Models: An Experimental Approach, Yuecheng Martin Yu, Alexander Pelaez, Karl R. Lang
Research Collection School Of Computing and Information Systems
This paper presents an experimental approach to compare the performance of alternative business process designs. We use an example case of an electronic group buying setting to demonstrate how our approach can be applied in practice. More specifically, we chose a standard business process, the sales process as implemented on a group buying platform, to illustrate how a business process may be redesigned in order to better meet the needs of customers. For that purpose, we introduce a social technology feature to support cooperation among buyers in the sales process and then analyze the performance impact of the proposed business …
Service Adaptation With Probabilistic Partial Models, Manman Chen, Tian Huat Tan, Jun Sun, Jingyi Wang, Yang Liu, Jing Sun, Jin Song Dong
Service Adaptation With Probabilistic Partial Models, Manman Chen, Tian Huat Tan, Jun Sun, Jingyi Wang, Yang Liu, Jing Sun, Jin Song Dong
Research Collection School Of Computing and Information Systems
Web service composition makes use of existing Web services to build complex business processes. Non-functional requirements are crucial for the Web service composition. In order to satisfy non-functional requirements when composing a Web service, one needs to rely on the estimated quality of the component services. However, estimation is seldom accurate especially in the dynamic environment. Hence, we propose a framework, ADFlow, to monitor and adapt the workflow of the Web service composition when necessary to maximize its ability to satisfy the non-functional requirements automatically. To reduce the monitoring overhead, ADFlow relies on asynchronous monitoring. ADFlow has been implemented and …
Scaling Bdd-Based Timed Verification With Simulation Reduction, Truong Khanh Nguyen, Tian Huat Tan, Jun Sun, Jiaying Li, Yang Liu, Manman Chen, Jin Song Dong
Scaling Bdd-Based Timed Verification With Simulation Reduction, Truong Khanh Nguyen, Tian Huat Tan, Jun Sun, Jiaying Li, Yang Liu, Manman Chen, Jin Song Dong
Research Collection School Of Computing and Information Systems
Digitization is a technique that has been widely used in real-time model checking. With the assumption of digital clocks, symbolic model checking techniques (like those based on BDDs) can be applied for real-time systems. The problem of model checking real-time systems based on digitization is that the number of tick transitions increases rapidly with the increment of clock upper bounds. In this paper, we propose to improve BDD-based verification for real-time systems using simulation reduction. We show that simulation reduction allows us to verify timed automata with large clock upper bounds and to converge faster to the fixpoint. The presented …
Mining Revision Histories To Detect Cross-Language Clones Without Intermediates, Lingxiao Jiang, Zhiming Peng, Lingxiao Jiang, Hao Zhong, Haibo Yu, Jianjun Zhao
Mining Revision Histories To Detect Cross-Language Clones Without Intermediates, Lingxiao Jiang, Zhiming Peng, Lingxiao Jiang, Hao Zhong, Haibo Yu, Jianjun Zhao
Research Collection School Of Computing and Information Systems
To attract more users on different platforms, many projects release their versions in multiple programming languages (e.g., Java and C#). They typically have many code snippets that implement similar functionalities, i.e., cross-language clones. Programmers often need to track and modify cross-language clones consistently to maintain similar functionalities across different language implementations. In literature, researchers have proposed approaches to detect cross-language clones, mostly for languages that share a common intermediate language (such as the .NET language family) so that techniques for detecting single-language clones can be applied. As a result, those approaches cannot detect cross-language clones for many projects that are …
On The Feasibility Of Detecting Cross-Platform Code Clones Via Identifier Similarity, Xiao Cheng, Lingxiao Jiang, Hao Zhong, Haibo Yu, Jianjun Zhao
On The Feasibility Of Detecting Cross-Platform Code Clones Via Identifier Similarity, Xiao Cheng, Lingxiao Jiang, Hao Zhong, Haibo Yu, Jianjun Zhao
Research Collection School Of Computing and Information Systems
More and more mobile applications run on multiple mobile operating systems to attract more users of different platforms. Although versions on different platforms are implemented in different programming languages (e.g., Java and Objective-C), there must be many code snippets that implement the similar business logic on different platforms. Such code snippets are called cross-platform clones. It is challenging but essential to detect such clones for software maintenance. Due to the practice that developers usually use some common identifiers when implementing the same business logic on different platforms, in this paper, we investigate the identifier similarity of the same mobile application …
Safegpu: Contract- And Library-Based Gpgpu For Object-Oriented Languages, Alexey Kolesnichenko, Christopher M. Poskitt, Sebastian Nanz
Safegpu: Contract- And Library-Based Gpgpu For Object-Oriented Languages, Alexey Kolesnichenko, Christopher M. Poskitt, Sebastian Nanz
Research Collection School Of Computing and Information Systems
Using GPUs as general-purpose processors has revolutionized parallel computing by providing, for a large and growing set of algorithms, massive data-parallelization on desktop machines. An obstacle to their widespread adoption, however, is the difficulty of programming them and the low-level control of the hardware required to achieve good performance. This paper proposes a programming approach, SafeGPU, that aims to make GPU data-parallel operations accessible through high-level libraries for object-oriented languages, while maintaining the performance benefits of lower-level code. The approach provides data-parallel operations for collections that can be chained and combined to express compound computations, with data synchronization and device …
Fine-Grained Detection Of Programming Students’ Frustration Using Keystrokes, Mouse Clicks And Interaction Logs, Hua Leong Fwa
Fine-Grained Detection Of Programming Students’ Frustration Using Keystrokes, Mouse Clicks And Interaction Logs, Hua Leong Fwa
Research Collection School Of Computing and Information Systems
Prolonged frustration leads to loss of confidence and eventual disinterest in the learning itself. The modelling of frustration in learning is thus important as it informs on the appropriate time to intervene to sustain the interest and motivation of students. To automatically detect learner’s frustration in a naturalistic learning environment, the novel use of keystrokes, mouse clicks and interaction patterns of students captured within the context of a tutoring system was proposed. The modelling approach was described and a comparison was made between the proposed model using Bayesian Network and the baseline Naïve Bayes model. With the formulation of an …
Satisfiability Modulo Heap-Based Programs, Quang Loc Le, Jun Sun, Wei-Ngan Chin
Satisfiability Modulo Heap-Based Programs, Quang Loc Le, Jun Sun, Wei-Ngan Chin
Research Collection School Of Computing and Information Systems
In this work, we present a semi-decision procedure for a fragment of separation logic with user-defined predicates and Presburger arithmetic. To check the satisfiability of a formula, our procedure iteratively unfolds the formula and examines the derived disjuncts. In each iteration, it searches for a proof of either satisfiability or unsatisfiability. Our procedure is further enhanced with automatically inferred invariants as well as detection of cyclic proof. We also identify a syntactically restricted fragment of the logic for which our procedure is terminating and thus complete. This decidable fragment is relatively expressive as it can capture a range of sophisticated …
An Interference-Free Programming Model For Network Objects, Mischael Schill, Christopher M. Poskitt, Bertrand Meyer
An Interference-Free Programming Model For Network Objects, Mischael Schill, Christopher M. Poskitt, Bertrand Meyer
Research Collection School Of Computing and Information Systems
Network objects are a simple and natural abstraction for distributed object-oriented programming. Languages that support network objects, however, often leave synchronization to the user, along with its associated pitfalls, such as data races and the possibility of failure. In this paper, we present D-Scoop, a distributed programming model that allows for interference-free and transaction-like reasoning on (potentially multiple) network objects, with synchronization handled automatically, and network failures managed by a compensation mechanism. We achieve this by leveraging the runtime semantics of a multi-threaded object-oriented concurrency model, directly generalizing it with a message-based protocol for efficiently coordinating remote objects. We present …
Domain-Specific Cross-Language Relevant Question Retrieval, Bowen Xu, Zhenchang Xing, Xin Xia, David Lo, Qingye Wang, Shanping Li
Domain-Specific Cross-Language Relevant Question Retrieval, Bowen Xu, Zhenchang Xing, Xin Xia, David Lo, Qingye Wang, Shanping Li
Research Collection School Of Computing and Information Systems
In software development process, developers often seek solutions to the technical problems they encounter by searching relevant questions on Q&A sites. When developers fail to find solutions on Q&A sites in their native language (e.g., Chinese), they could translate their query and search on the Q&A sites in another language (e.g., English). However, developers who are non-native English speakers often are not comfortable to ask or search questions in English, as they do not know the proper translation of the Chinese technical words into the English technical words. Furthermore, the process of manually formulating cross-language queries and determining the weight …
A Graph-Based Semantics Workbench For Concurrent Asynchronous Programs, Claudio Corrodi, Alexander Heußner, Christopher M. Poskitt
A Graph-Based Semantics Workbench For Concurrent Asynchronous Programs, Claudio Corrodi, Alexander Heußner, Christopher M. Poskitt
Research Collection School Of Computing and Information Systems
A number of novel programming languages and libraries have been proposed that offer simpler-to-use models of concurrency than threads. It is challenging, however, to devise execution models that successfully realise their abstractions without forfeiting performance or introducing unintended behaviours. This is exemplified by Scoop—a concurrent object-oriented message-passing language—which has seen multiple semantics proposed and implemented over its evolution. We propose a “semantics workbench” with fully and semi-automatic tools for Scoop, that can be used to analyse and compare programs with respect to different execution models. We demonstrate its use in checking the consistency of semantics by applying it to a …
Codehow: Effective Code Search Based On Api Understanding And Extended Boolean Model (E), Fei Lv, Jian-Guang Lou, Shaowei Wang, Dongmei Zhang, Jainjun Zhao
Codehow: Effective Code Search Based On Api Understanding And Extended Boolean Model (E), Fei Lv, Jian-Guang Lou, Shaowei Wang, Dongmei Zhang, Jainjun Zhao
Research Collection School Of Computing and Information Systems
Over the years of software development, a vast amount of source code has been accumulated. Many code search tools were proposed to help programmers reuse previously-written code by performing free-text queries over a large-scale codebase. Our experience shows that the accuracy of these code search tools are often unsatisfactory. One major reason is that existing tools lack of query understanding ability. In this paper, we propose CodeHow, a code search technique that can recognize potential APIs a user query refers to. Having understood the potentially relevant APIs, CodeHow expands the query with the APIs and performs code retrieval by applying …
Challenges In Analyzing Software Documentation In Portuguese, Christoph Treude, Carlos A. Prolo, Fernando Figueira Filho
Challenges In Analyzing Software Documentation In Portuguese, Christoph Treude, Carlos A. Prolo, Fernando Figueira Filho
Research Collection School Of Computing and Information Systems
Many tools that automatically analyze, summarize, or transform software artifacts rely on natural language processing tooling for the interpretation of natural language text produced by software developers, such as documentation, code comments, commit messages, or bug reports. Processing natural language text produced by software developers is challenging because of unique characteristics not found in other texts, such as the presence of code terms and the systematic use of incomplete sentences. In addition, texts produced by Portuguese-speaking developers mix languages since many keywords and programming concepts are referred to by their English name. In this paper, we provide empirical insights into …
Contract-Based General-Purpose Gpu Programming, Alexey Kolesnichenko, Christopher M. Poskitt, Sebastian Nanz, Bertrand Meyer
Contract-Based General-Purpose Gpu Programming, Alexey Kolesnichenko, Christopher M. Poskitt, Sebastian Nanz, Bertrand Meyer
Research Collection School Of Computing and Information Systems
Using GPUs as general-purpose processors has revolutionized parallel computing by offering, for a large and growing set of algorithms, massive data-parallelization on desktop machines. An obstacle to widespread adoption, however, is the difficulty of programming them and the low-level control of the hardware required to achieve good performance. This paper suggests a programming library, SafeGPU, that aims at striking a balance between programmer productivity and performance, by making GPU data-parallel operations accessible from within a classical object-oriented programming language. The solution is integrated with the design-by-contract approach, which increases confidence in functional program correctness by embedding executable program specifications into …
Memes As Building Blocks: A Case Study On Evolutionary Optimization + Transfer Learning For Routing Problems, Liang Feng, Yew-Soon Ong, Ah-Hwee Tan, Ivor W. Tsang
Memes As Building Blocks: A Case Study On Evolutionary Optimization + Transfer Learning For Routing Problems, Liang Feng, Yew-Soon Ong, Ah-Hwee Tan, Ivor W. Tsang
Research Collection School Of Computing and Information Systems
A significantly under-explored area of evolutionary optimization in the literature is the study of optimization methodologies that can evolve along with the problems solved. Particularly, present evolutionary optimization approaches generally start their search from scratch or the ground-zero state of knowledge, independent of how similar the given new problem of interest is to those optimized previously. There has thus been the apparent lack of automated knowledge transfers and reuse across problems. Taking this cue, this paper presents a Memetic Computational Paradigm based on Evolutionary Optimization + Transfer Learning for search, one that models how human solves problems, and embarks on …
Neural Modeling Of Sequential Inferences And Learning Over Episodic Memory, Budhitama Subagdja, Ah-Hwee Tan
Neural Modeling Of Sequential Inferences And Learning Over Episodic Memory, Budhitama Subagdja, Ah-Hwee Tan
Research Collection School Of Computing and Information Systems
Episodic memory is a significant part of cognition for reasoning and decision making. Retrieval in episodic memory depends on the order relationships of memory items which provides flexibility in reasoning and inferences regarding sequential relations for spatio-temporal domain. However, it is still unclear how they are encoded and how they differ from representations in other types of memory like semantic or procedural memory. This paper presents a neural model of sequential representation and inferences on episodic memory. It contrasts with the common views on sequential representation in neural networks that instead of maintaining transitions between events to represent sequences, they …
Detection And Classification Of Malicious Javascript Via Attack Behavior Modelling, Yinxing Xue, Junjie Wang, Yang Liu, Hao Xiao, Jun Sun, Mahinthan Chandramohan
Detection And Classification Of Malicious Javascript Via Attack Behavior Modelling, Yinxing Xue, Junjie Wang, Yang Liu, Hao Xiao, Jun Sun, Mahinthan Chandramohan
Research Collection School Of Computing and Information Systems
Existing malicious JavaScript (JS) detection tools and commercial anti-virus tools mostly use feature-based or signature-based approaches to detect JS malware. These tools are weak in resistance to obfuscation and JS malware variants, not mentioning about providing detailed information of attack behaviors. Such limitations root in the incapability of capturing attack behaviors in these approches. In this paper, we propose to use Deterministic Finite Automaton (DFA) to abstract and summarize common behaviors of malicious JS of the same attack type. We propose an automatic behavior learning framework, named JS∗ , to learn DFA from dynamic execution traces of JS malware, where …
Verifying Parameterized Timed Security Protocols, Li Li, Jun Sun, Yang Liu, Jin Song Dong
Verifying Parameterized Timed Security Protocols, Li Li, Jun Sun, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Quantitative timing is often explicitly used in systems for better security, e.g., the credentials for automatic website logon often has limited lifetime. Verifying timing relevant security protocols in these systems is very challenging as timing adds another dimension of complexity compared with the untimed protocol verification. In our previous work, we proposed an approach to check the correctness of the timed authentication in security protocols with fixed timing constraints. However, a more difficult question persists, i.e., given a particular protocol design, whether the protocol has security flaws in its design or it can be configured secure with proper parameter values? …
Heuristic Collective Learning For Efficient And Robust Emergence Of Social Norms, Jianye Hao, Jun Sun, Dongping Huang, Yi Cai, Chao Yu
Heuristic Collective Learning For Efficient And Robust Emergence Of Social Norms, Jianye Hao, Jun Sun, Dongping Huang, Yi Cai, Chao Yu
Research Collection School Of Computing and Information Systems
In multiagent systems, social norms is a useful technique in regulating agents’ behaviors to achieve coordination or cooperation among agents. One important research question is to investigate how a desirable social norm can be evolved in a bottom-up manner through local interactions. In this paper, we propose two novel learning strategies under the collective learning framework: collective learning EV-l and collective learning EV-g, to efficiently facilitate the emergence of social norms. Experimental results show that both learning strategies can support the emergence of desirable social norms more efficiently in a much broader range of multiagent interaction scenarios than previous work, …
Privacycanary: Privacy-Aware Recommenders With Adaptive Input Obfuscation, Thivya Kandappu, Arik Friedman, Roksan Borelli, Vijay Sivaraman
Privacycanary: Privacy-Aware Recommenders With Adaptive Input Obfuscation, Thivya Kandappu, Arik Friedman, Roksan Borelli, Vijay Sivaraman
Research Collection School Of Computing and Information Systems
Recommender systems are widely used by online retailers to promote products and content that are most likely to be of interest to a specific customer. In such systems, users often implicitly or explicitly rate products they have consumed, and some form of collaborative filtering is used to find other users with similar tastes to whom the products can be recommended. While users can benefit from more targeted and relevant recommendations, they are also exposed to greater risks of privacy loss, which can lead to undesirable financial and social consequences. The use of obfuscation techniques to preserve the privacy of user …
Web Application Vulnerability Prediction Using Hybrid Program Analysis And Machine Learning, Lwin Khin Shar, Lionel Briand, Hee Beng Kuan Tan
Web Application Vulnerability Prediction Using Hybrid Program Analysis And Machine Learning, Lwin Khin Shar, Lionel Briand, Hee Beng Kuan Tan
Research Collection School Of Computing and Information Systems
Due to limited time and resources, web software engineers need support in identifying vulnerable code. A practical approach to predicting vulnerable code would enable them to prioritize security auditing efforts. In this paper, we propose using a set of hybrid (staticþdynamic) code attributes that characterize input validation and input sanitization code patterns and are expected to be significant indicators of web application vulnerabilities. Because static and dynamic program analyses complement each other, both techniques are used to extract the proposed attributes in an accurate and scalable way. Current vulnerability prediction techniques rely on the availability of data labeled with vulnerability …
Event Analytics, Jin Song Dong, Jun Sun, Yang Liu, Yuan-Fang Li
Event Analytics, Jin Song Dong, Jun Sun, Yang Liu, Yuan-Fang Li
Research Collection School Of Computing and Information Systems
The process analysis toolkit (PAT) integrates the expressiveness of state, event, time, and probability-based languages with the power of model checking. PAT is a self-contained reasoning system for system specification, simulation, and verification. PAT currently supports a wide range of 12 different expressive modeling languages with many application domains and has attracted thousands of registered users from hundreds of organizations. In this invited talk, we will present the PAT system and its vision on “Event Analytics” (EA) which is beyond “Data Analytics”. The EA research is based on applying model checking to event planning, scheduling, prediction, strategy analysis and decision …
A Palm Vein Identification System Based On Gabor Wavelet Features, Ran Wang, Guoyou Wang, Zhong Chen, Zhigang Zeng, Yong Wang
A Palm Vein Identification System Based On Gabor Wavelet Features, Ran Wang, Guoyou Wang, Zhong Chen, Zhigang Zeng, Yong Wang
Research Collection School Of Computing and Information Systems
As a new and promising biometric feature, thermal palm vein pattern has drawn lots of attention in research and application areas. Many algorithms have been proposed for authentication since palm vein has special characteristics, such as liveness detection and hard to forgery. However, the detection accuracy of palm vein quite depends on the preprocessing and feature representation, which is supposed to be translation and rotation invariant to some extent. In this paper, we proposed an effective method for palm vein identification based on Gabor wavelet features which contains five steps: image acquisition, ROI detection, image preprocessing, features extraction, and matching. …
Diamonds Are A Girl's Best Friend: Partial Order Reduction For Timed Automata With Abstractions, Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, Jun Sun
Diamonds Are A Girl's Best Friend: Partial Order Reduction For Timed Automata With Abstractions, Henri Hansen, Shang-Wei Lin, Yang Liu, Truong Khanh Nguyen, Jun Sun
Research Collection School Of Computing and Information Systems
A major obstacle for using partial order reduction in the context of real time verification is that the presence of clocks and clock constraints breaks the usual diamond structure of otherwise independent transitions. This is especially true when information of the relative values of clocks is preserved in the form of diagonal constraints. However, when diagonal constraints are relaxed by a suitable abstraction, some diamond structure is re-introduced in the zone graph. In this article, we introduce a variant of the stubborn set method for reducing an abstracted zone graph. Our method works with all abstractions, but especially targets situations …
Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong
Scc-Based Improved Reachability Analysis For Markov Decision Processes, Lin Gui, Jun Sun, Songzheng Song, Yang Liu, Jin Song Dong
Research Collection School Of Computing and Information Systems
Markov decision processes (MDPs) are extensively used to model systems with both probabilistic and nondeterministic behavior. The problem of calculating the probability of reaching certain system states (hereafter reachability analysis) is central to the MDP-based system analysis. It is known that existing approaches on reachability analysis for MDPs are often inefficient when a given MDP contains a large number of states and loops, especially with the existence of multiple probability distributions. In this work, we propose a method to eliminate strongly connected components (SCCs) in an MDP using a divide-and-conquer algorithm, and actively remove redundant probability distributions in the MDP …
Teaching Tip: The Flipped Classroom, Heng Ngee Mok
Teaching Tip: The Flipped Classroom, Heng Ngee Mok
Research Collection School Of Computing and Information Systems
The flipped classroom has been gaining popularity in recent years. In theory, flipping the classroom appears sound: passive learning activities such as unidirectional lectures are pushed to outside class hours in the form of videos, and precious class time is spent on active learning activities. Yet the courses for information systems (IS) undergraduates at the university that the author is teaching at are still conducted in the traditional lecture-in-class, homework-after-class style. In order to increase students’ engagement with the course content and to improve their experience with the course, the author implemented a trial of the flipped classroom model for …