Posts
Please also see my Modern Deduction Blog for results specific to the NSF PPoSS project.-
My Rejected NSF CAREER Proposal
My NSF CAREER proposal was rejected, and I’m making it publicly available: Micinski CAREER Proposal (PDF). The proposals scores were VG/G, VG/G, and E/VG. While the proposal was rejected as competitive, my position is that the proposal is nicely written and addresses a serious and important challenge in a credible...
-
Why Study CS? Thoughts on LLM-assisted software engineering
Dear students of Computer Science, Almost everything everyone is telling you about LLMs is probably wrong. Some tell you it’s glorified autocomplete, others say it will cure cancer or prove the loftiest theorems. As with many mass-market takes, these claims contain a grain of truth–but they miss the point. I...
-
Build a Compiler in Five Projects
Class website here: https://kmicinski.com/cis531-f25 Are you interested in building a compiler? Learning how functional languages are implemented? Gaining a bit of practical experience with x86-64 assembly language? If so, I invite you to try your hand at the projects in my class, CIS531. CIS531 is a masters-level class on compiler...
-
Why Tail-Recursive Functions are Loops
One story every computing enthusiast should hear is the lesson of how loops and tail-recursion are equivalent. We like recursive functions because they’re amenable to induction, and we can derive them in a way that is in direct correspondence with the definition of the datatype over which they recur. We...
-
Modern Deduction Post 1: Chain-Forward Computation
Our setting is logic programming, a field which attempts to design programming languages whose semantics have a close relationship to formal logic. The reason we might want to do this is that it suits our application domain more precisely than an implementation in a traditional programming language. Thus, using a...
-
Modern Deduction Post 0: Prologue
Over the past few years, my collaborators and I have been exploring the design of high-performance logic programming engines for a wide variety of tasks, including program analysis (points-to analysis, abstract interpretation), graph analytics (transitive closure, PageRank), and security (binary code similarity, disassembly, and decompilation). We (myself, my collaborators, and...
-
Mid-Point Review Materials
This page holds my “year 3 review” materials for evaluation and promotion at Syracuse University. My detailed personal statement (including teaching and research statements) is here My current CV is linked here A (~22MB) zip file linked here gives the full review packet, including CV, papers, and my personal statement....
-
Certifying Interpreters in Racket
When I began programming, I read a copy of Richard Steven’s “Programming in the UNIX Environment.” Ultimately, my early experimentations with C were a failure; however, I later read David Beazley’s “Python: Essential Reference,” and was quickly able to pick up the UNIX API via it’s much simpler (admittedly, largely...
-
Why I hope you'll submit to Scheme Workshop
Link to this year’s Scheme Workshop CFP This year marks the twentieth anniversary of the workshop on Scheme and Functional Programming. The Scheme Workshop represents a diverse community of hackers, academics, and enthusiasts. The workshop offers a forum to share insights, experience, and technical developments of and within the Scheme...
-
Why Does Netflix See my Facebook Picture?
The other day I updated my Facebook profile picture. The thing I didn’t realize was that when I changed it, Netflix also got it: This is pretty jarring. Where was the “share this with Netflix” button that I pressed? Of course, the answer is that it’s right here: It’s buried...
-
Video: Exploiting Use After Free (UAF) vulnerabilities
Obligatory: I must point out that my inspiration for this post was a really nice video on YouTube. I don’t claim to have invented this idea, I just wanted to explain it in a way that makes sense to me (although the YouTuber likely does a better job than I)....
-
Job materials for 2017
I’m applying to colleges and universities again in 2017. I’m very happy at Haverford, but I’m on the lookout for a tenure-track spot at a place that has students and colleagues that will excite me in the same way I’m feeling right now: My research statement (4 12-point pages) My...
-
All About Git
I’m giving a college-wide talk for FIG (Fig is Good) tonight. FIG is a student computing group. I’m hoping to record the talk, but for now I’ll just put the slides here.
-
My new cybersecurity course at Haverford (Spring 2017)
You can also download this syllabus as a PDF. Computer Security: Attacks and Defenses (CMSC 323 at Haverford) Prerequisites: Experience in C programming: E.g., CMSC245 at Haverford or CMSC246 at Bryn Mawr Experience with or willingness to learn learn new languages (Python, SQL, JavaScript, etc..) Workload: 3 lecture hours per...
-
Writing tip: say the text back to you
Here’s the tip: have your computer read your writing back to you. Listen to how it sounds. Then, iterate until it conveys what you’d like to hear. On a mac, you can do this it like this: say -r words_per_minute "My speech goes here" I do this to either: Read...
-
How to Succeed in Grad School
I gave this talk on August 24, 2017, to incoming grad students at the University of Maryland, College Park. Full slides available here
-
Here: Have Some PLUM Scrum
This post is about transparency with your advisor. It seems like most problems that PhD students face boil down to communication and transparency: students work on something the advisor doesn’t expect, the advisor has different expectations for number of papers required to graduate, student collaborates with someone when the advisor...
-
Appreciating Research as Problems
Recently I reflected on the kinds of problems I’ve worked on during my PhD, and in doing so realized that I likely did not fully appreciate what research was until rather recently. Research is about identifying and solving novel, important, and generalizable problems inherent in nature. Looking back on the...
-
The nonobvious -- but important -- aspects of teaching (for me)
I recently got motivated to look up teaching reviews for members of our department (and myself) on various websites our students frequent. Something occurred to me that I had previously suspected but hadn’t clearly articulated in my head: the parts of teaching that I enjoyed most weren’t necessarily the most...
-
Program Visualization as Abstract Interpretation
For this past semester, I’ve been thinking in a semi-principaled way about how we should visualize program executions. For example, how should we visualize this program: let id x = x in let g x = id x let check_zero y = if y = 0 then bad () else...
-
Half-Baked Ideas on The Future of Static Analysis and Security
It is well known that security policies for programs (such as noninterference) are not properties of a single run, but rather of properties about sets of runs. For example, the following program uses a so-called implicit flow to exfiltrate the value of its secret input: input(secret) if (secret == 0)...
-
The Environment Problem and Abstract Counting
Over the weekend I attempted to read a paper by Matt Might called Logic Flow Analysis. Logic Flow Analysis promises to marry constraint solvers and abstract interpretation so that they play off each other to produce better analysis results. Unfortunately, I fell somewhat flat on this, as the amount of...
-
Efficient SAT Solving
The Boolean satisfiability problem is simply stated: Given a set of propositional formulas, decide whether or not there is an assignment to the variables in the formula such that the formula is satisfied (true). This basically says: given a large set of constraints with AND and ORs, can you find...
-
On Understanding Coinduction
Here’s the basic story: Induction is about finite data, co-induction is about infinite data. The typical example of infinite data is the type of a lazy list (a stream). For example, lets say that we have the following object in memory: let (pi : int list) = (* some function...
subscribe via RSS